m MAC TR-136 FUNCTIONAL DOMAINS OF APPLICATIVE LANGUAGES Stephen A. Ward September 1974 This research was supported by the Advanced Research Projects Agency of the Department of Defense under ARPA Order No. 2095 which was monitored by ONR Contract No. N00014- 70-A-0362-O0O6 MASSACHUSETTS INSTITUTE OF TECHNOLOGY PROJECT MAC CAMBRIDGE MASSACHUSETTS 02139 This empty page was substituted for a blank page in the original document. ACKNOWLEDGEMENT The author gratefully acknowledges the assistance of his Thesis Committee in this work. Professors Jack Dennis and Joseph Weizenbaum, his readers, provided helpful suggestions and encouragement during the course of the thesis research. The author feels a special indebtedness to his thesis supervisor, Professor Michael Dertouzos, for his essential contributions to the direction, motivation, and technical content of this work. Particular thanks are due the author's wife, Debbie, whose constant support and encouragement have thus far been rewarded by a depressingly long period as the wife of a student. The author is grateful to the Department of Electrical Engineering for the Instructorship under which much of this research was carried out. This work was also supported in part by Project MAC, an M.I.T. research program sponsored by the Advanced Research Projects Agency, Department of Defense, under Office of Naval Research Contract N00014-70-A-0362-GO06. This empty page was substituted for a blank page in the original document. FUNCTIONAL DOMAINS OF APPLICATIVE LANGUAGES Abstract The expressive power of a particular applicative language may be characterized by the set of abstract functions di- rectly representable in that language. The common FUNARG and applicative order problems are scrutinized in this way, and the effects of these weaknesses are inexpressibil ity of classes of functions. related to the Certain computable functions which are inexpressible in the lambda calculus are identified, and it is established that the interpretation of these functions requires a mechanism fundamentally equivalent to multiprocessing. The EITHER construct is proposed as an extension to the lambda calculus, and several theories including this mechanism are presented and proved consistent (in the sense that they introduce no new equivalences into the lambda calculus). conversi on , this adjunct normal forms in A syntactic analog to the Scott construction, is developed in conjunction with these theories; allows reduction of expressions having no the usual lambda calculus to finite normal form approximations of the expressions. This leads naturally to a technique for proving the extensional equivalence of lambda calculus expressions which are not interconvertible. title submitted *This report reproduces a thesis of the same to the Department of Electrical Engineering, Massachusetts Institute of Technology, in partial fulfillment of the requirements for the degree of Doctor of Philosophy, June 1974 / -5- Table of Contents Table of Contents Introduction 1.1: Programming Language Semantics Applicative Languages The Thesis: Statement of the Problem Outline of the Thesis Functional Domains 1.5.1: Intuitive Criteria for Functions 1.5.2: Functional Domain: Definition 1.2: 1.5: : Interpreter Structure and Expressive Power 2.1: Syntax of Models 2.2: Curried Functions 2.3: The FUNARG Problem 2.3.1: The S model 2.3.2: Arithmetic Completeness of S 2.3.3: Functional Incompleteness of S 2.4: Evaluation Order 2.4.1: The T Model 2.4.2: Functional Incompleteness of T 2.5: The N model 2.5.1: Axioms for the Lambda Calculus 2.5.2: Normal order: Substitution 2.5.2.1: The M Evaluator 2.5.2.2: Axiomatic Consistency of N 2.6: Functional Domain of N 2.7: Summary : Motivation for a Multi-valued Semantics 3.1: Necessity of non- functions: WHICHFF 3.2: Coding primitives: The C model 3.2.1: The Turing-machine Tar Pit 3.2.2: Functionality of DECODE 3.2.2.1: LAMBDA-free AEs 3.2,2.2: An Enumeration of D E model: Multiprocessing primitives The Intuitive Paradox Multi-valued Semantic Elements 5.1: Domains of Specification 5.2: EITHER and the Lambda Calculus The Power Set Domain Interpretation of F* 3.8: Computable elements of F* 3.9: Summary 3. 3. 3-5 3 3.6 :l 4: Theories of EITHER-conversion 4.1: Preliminary Definitions 4.2: The Either-R Theories 4.2.1: Properties of Either Theories 4.2.2: EITHER and Evaluation Order 4.2.3: Consistency of Either-R 4.3: Summary 5: *-Conversion 5.1: The R- # Theories 5.1.1: Significance of normal forms 5.1.2: Theorem on Normal Forms 5.1.3: Relation to the Lambda Calculus 5.1.4: Consistency of R-* Theories 5.2: Applications to the Lambda Calculus 5.3: Summary 6: The Either-R-* Theories 6.1: Consistency of Either-R-« 6.2: Relation of » to EITHER 6.3: Evaluators for E 6.4: Summary :able of Contents -6- 7: The Either-K Theories 7 7.2 7. ■7 K-abs traction Consistency of Either-K Theories Functional Domains of Either-K Summary 3: Summary and Conclusions 1 i.2 i. 3 Summary Conclusions Directions of Future Research 9: References 10: Biographical note 101 101 1 10 1 1 1 113 1 1 1 1 1 17 120 12i This empty page was substituted for a blank page in the original document. -7- Chapter 1 : Introduction 1.1: Programming Language Semantics . The semantics of a programming language may be viewed as a theory which accounts for the behavior of programs written in that lakngua^e. An,, interpreter for a language L is a model for the semantics .of L, and a language whose semantics is incomplete (in the sense of an incomplete theory) ,may have many "correct" interpreters which behave differently Just as an incomplete theory may have disparate models. We find that the usual more specific definitions of semantics (e.g. "the relation between expressions and the objects vhich they denote") make assumptions about the structure of a universe of "meanings" which are difficult to justify in the general case, where side effects, assignment, and transfers of ceotroli mast biPiee&unted for 3emant Really. Such consideration* motivate the reattfeMon of the present ' work to applicative languages. Serious concern for formal semantics is not usually an important consideration in the architecture of practical languages. TypicaJ.lv, a language is designed, largely by pragmatic considerations and the formal statement of its semantics is either abandoned entirely or postponed until the more important implementation issues are sorted out. The subsequent semantic formalization of th* language inevitably becomes a major task, and the complexity, volume, and inscrutability of the result may constrain its "usefulness, A classic example of such an undertaking is the description of PL/1 in the Vienna Definition Language[ 24], An alternative technique of language design, exemplified to some extent in LISP[26] and its recent derivatives, Involves the specification of the pragmatics of a language after decisions on some particular concise semantics have been made. Unfortunately languages so designed tend to have serious defects from a practical point of view and are abandoned or complicated by the addition of aj. 1122. mechanisms to make them more useful. -8- 1.1 The designer of a language is thus confronted with a choice between concise semantics and practical usability, and he justifiably tends to opt for the latter alternative. The extent to which semantic considerations may be reconciled with practical issues remains an important open question, and the development of practical languages with concise, elegant semantics is the long term goal of much of Computer Science research. The problem is being attacked from two discernible directions: (i) semantic formalisms which deal with the mechanisms of extant practical languages, such as the analysis of uninterpreted schema ta[9, 8, 13, 17,25] ; and (ii) the adaptation of existing formalisms to very simple model languages such as the lambda calculus[2,3,5,15,22]. The work reported here falls naturally into the second category. 1.2: Applicative Languages Familiar concepts of mathematics provide an informal semantics for many aspects of computer languages. Manuals for most programming languages relate various program constructs to such notions as real nu«b«rs, arithmetic, and functions, with which the reader is presumed to be acquainted. Often terminology and notation are borrowed from mathematics, implying some informal relation between, say, a FORTRAN "function" and the common mathematical notion of f met ion. This relation is only approximate, since for example no mathematical analog has been established for the FORTRAN function which prints its argument on the teletype. In order to formalize the relationship between program constructs and mathematical notions, then, we focus our attention on the highly restricted class of applicative languages. The semantic bases of applicative languages are the theories of mathematical functions, and the constructs of these languages are restricted to simple analogs of the related mathematical notions. Each applicative language provides a syntactic formalism for the representation of functions and their application to arguments, and the semantics of an applicative language is in general a rule for the association of expressions, constructed according to this formalism, with values from an abstract semantic domain containing functions and constants. Formalizing a consistent semantics for an 1.2 -9- applicative language appears to be an easy first step in pursuing the general problem of programming language semantics; since set theory provides satisfactory semantic domains, all that remains is the seemingly simple association of expressions with set theoretic functions and constants. Yet even this simple problem is plagued with explications, add it is only in recent years that progress has been made in thin are* isKargely due to techniques developed by Dana ScottlS ,G*22h In tact, -tits' Usual set theoretic characterization of functions is not so well adapted to the semantics of applicative languages as one might suspect: type restrictions, placed on set theoretic functions in order to avoid Russel 's Paradox, are difficult to reconcile with the natural proclivity of applicative languages for the self-application of functions. The work of Scott justifies our optimism that such problems^ are traetabley and that the semantics ofs applicative languages may be based on the mathematics of functions. Th* extension of tha reciting semantics to non-applicative mechanisms such as assignment and side effects however, remains ah area of grave uncertainty, and it seems likely that theories of functions will ultimately prove to be inadequate bases for the semantics of programming languages in general. In the meantime, however, applicative languages and their fmctionnl aew^ie 4omaioa ; ape probably the closest we have cane to a successful programming language semantics, and we feel that there is much insight to be gained from further exploration of this area. The semantics of an„ applicative language L,thi6 t pajr bai^iewed as a mapping between the set of walfca expressions ia ; la (the djoto ^ 4iS2flittfiS. of h) and and a semantic detain of abatriot functions and osnntants. * -consequence of the Turing Universality of L is that this napping *uat 4w many to one; each abstract semantic element has, in general, infinitely many representations in the language L. The semantic mapping thus leads naturally to a notion of semantic equivalence between expressions in L, partitioning the domain of discourse of L into equivalence classes each of which corresponds to a single abstract semantic element. -10- 1.3 1.3: The Thesis: Statement of the Problem The problem which this thesis addresses is the characterization of the expressive power of an applicative language in terms of the structure of its abstract semantic domain. This process generally involves relating specific applicative' language features to the expressibility of particular classes of functions, e.g. the solution of the FUHARG problem to the expressibility of functions mapping integers onto an infinite range of senantieally distinct functions. ■ ' -, This work focuses on a very few specific language mechanisms, with particular attention given to an applicative analog of multiprocessing. Partial answers are provided to such questions as: 1) Are there functions whose computability depends fundamentally on a noti&n analogous to multiprocessing? 2) What applicative mechanisms are necessary for the expression of such functions, and is the impact of these mechanisms on the structure of the semantic domain? 3) What is such relationship between such multiprocessing constructs and other issue* of applicative language evaluation, such as evaluation order? The work presented here might be characterized as a search for an applicative language L which is ffunotlonallr complete in > the saaaalfehat every computable function definable on the semantic domain of L is expressible in L -- our reluctance. to cite this as the principal goal of the thesis is probably due to our failure to find such a language. 1.4: Outline of the Thesis The organization of the remaining chapters is as follows: Chapter 2 develops the basic framework through the presentation of three interpreters for applicative languages, designated S (stack environment), T (tree environment), and N (normal order). Each interpreter exemplifies 1.4 -11- a typical language limitation and each is- used to relate a specific language characteristic to the expressibility of a particular class of functions. Chapter 3 demonstrates a particular computable function which is inexpressible both in N and in the lambda calculus, and relates this inexpressibility to the semantic requirement that an expression in these languages have at most a single value. Two alternative language extensions are discussed, each of which solves this- specific expressibility problem. The solutions involve, respectively, primitives for coding the representation of functions as integers and a multiprocessing primitive called EITHER. Each of these extensions requires modification of the structure of the semantic domain, with the use of coding leading to drastic and undesirable consequences. For this and related reasons, EITHER is chosen. To account for the semantics of EITHER, the semantic domain of N is expanded into a power set and each expression X is associated semantically with an enumerate le set containing the admissible values of X. The formalization of EITHER-augmented languages may procede in several ways, differing in the restrictions placed on evaluation order. Chapters 4, 5, 6, and 7 deal with certain formal theories, based on the lambda calculus, for the reduction of expressions involving the EITH2R construct: Chapter 4 provides basic definitions and presents the Either-R Theory, in which lambda conversion is allowed only in expressions whose arguments are in normal form. This restriction is motivated by the intuitive desire to maintain the distributivity of functions over terms of an EITHER clause, but it limits the power of languages based on this theory. Chapter 5 develops a theory of '-conversion, designed to mitigate the limitations imposed by the restricted lambda conversion of the Either-R Theory. The element • is introduced as a canonical representation of every nonterminating computation, and a syntactic mechanism is provided for the reduction of expressions to approximations which are in normal form. The use of •-conversion provides techniques for proving certain relationships in the conventional lambda calculus. This chapter presents -12- 1.H results which are of interest independently of their relation to the development of the Either theories. Chapter 6 presents the Either-R-« theory, combining the EITHER mechanism with "-conversion, and establishes its consistency. While this system retains the restriction on lambda conversion* it has the power of the lambda calculus augmented by the EITHER primitive. Thus, languages based on Either-fl-» solve the specific expressibility problem raised in Chapter 3- Interpreters and semantics for such languages are discussed. Chapter 7 presents the Either-K theory, which combines the EITHER construct with unrestricted lambda conversion. Significant semantic differences between the Either-R and Either-K theories are noted, and it is informally observed that the removal of the restriction on lambda conversion leads to the expressibility of certain functions which are inexpressible in the Either-R-* languages. The last chapter summarizes the results of this work and proposes avenues for future research. 1.5: Functional Domains An underlying assumption of this research is that the fundamental semantic intent of applicative languages is to provide computational models of mathematical functions. As a consequence of this assumption, we are inclined to view functions in an applicative language as approximations or models of abstract mathematical functions, and to treat any disparity between the behavior of the computationa'l model and the corresponding mathematical function as a "bug" or idiosyncrasy in the language. The thrust of this research is aimed at the limitations of particular applicative languages as models of systems of mathematical functions. We begin by specifying, in the next section, criteria which must be obeyed by applicative functions to be intuitively satisfactory as models of mathematical functions, and then distinguish for each applicative language L that subset of the domain of L containing only such intuitively satisfying functions. We call such a subdomain of L a functional domain of L. 1.5.1: Intuitive Criteria for Functions R.- ^stricting our attention for the moment to unary (single argument) functions, vve note that 1) A function £ is a ffiafifiifl* from a domain D f to a range R . The set-theoretic model of I is a set of ordered pairs, {. .fo r >. . . } , such that £[D 1 ]=R 1 if and only if KD^R^.i. an element of £. 2) A function f may be partial over domain D, i.e., there may be elements D. in D such that fjD^ is undefined; this corresponds to the practical * situation of a nonterminal ing computation or "a computation which results in an error condition. We shall refer to such a computation as divergent. 3) If f and g. provide the same mapping, then they are the same function. *0 & is a aiifcafiJL of £ (in the set-theoretic sense) if and only if for every D t in the domain of g., gj^^ implies fjD^aR . Given a language L and a function £, a principal intuitive requirement is the distinction between the function £ and the vario** algorithms (or expressions in L) which may be used to compute £. A ma joif SoAplicatlon in the semantics of applicative languages arises from this many-to-one correspondance between algorithms and functions, particularly in light of the well known un decidability of equivalences between algorithms. 1.5.2: Functional Domain: Definition The intuitive considerations of the previous nation motivate the following definition: Deffl 1,1: A iimciianai dfiBain F is a set containing the set M of natural numbers and computable functions, 1 along with an equivalence relation - such that: tvS^ff^? 6 ^ 10311 ^ 313 ^ 1 ' we sna11 use the term function with no implied no^C? 3 ^ 10 ^"?: thus Unctions include fun ctionaTsoriFbitrary order consistent with the typeless character of the applicative languages considered -14- 1.5.2 1) if x is in N or i is in N, then x~y if and only if x=y. 2) if neither x_ nor y_ is in N, then x~y if and only if for every z in F, 2lCs.1~Y.C2.] or both diverge together. 3) if x~y_, then for every z_ in F, z_[xj~alvj of both diverge together. Clause (1) simply asserts that different numbers, eg 2 and 3, are semantically different objects. Clause (2) asserts that any object in F that is not a number is a function, and moreover that functions are semantically equivalent if and only if they perform equivalent computations for every set of arguments. Clause (3) insists that the application of a function to semantically equivalent arguments yield semantically equivalent values. An expression z, is said to be fuggtlonqj , over t;he domain F if, for every choice of x_ and y_ in F, x_~y_ implies that z_[xj~z_[yj or both computations diverge together. Thus (3) is the requirement that every function in a functional domain F be functional over F. We note that the equivalence relation ~ is not, in general, computable. Furthermore, there may be elements x. and y_ in F sueh that x.~y_ is not defined, that i£, such that neither x_~v_ nor ~(x.~y_) ;;. is derivable from the above definition. This definition is rather more specific than necessary. The choice of natural numbers as a basis of semantically distinct constants, rather than, say, character strings or floating point numbers, is arbitrary. In dealing with the lambda calculus we could make the apparently stronger requirement that normal form expressions be semantically distinct, rather than just the particular normal form expressions whiqh are numeric constants; however it happens that the two alternatives are entirely equivalent in the context of our model languages, and our present definition is the less dependent on particular syntactic considerations. 2 -15- Chapter 2: Interpreter Structure and Expressive Power In this chapter several illustrative interpreters for applicative languages are presented, and compromises in their implementation are related to the inexpressibility of certain functions. The model interpreters are taken from Dertouzos[3l where they are discussed and motivated in greater detail. 2.1: Syntax of Models The essential components of an applicative language syntax are conventions for the representation and application of functions. Typical applicative languages provide for the representation of functions by either or" both of the following means: 1) A set of reserved symbols designating w^ilUJtt' XtofitlflDl whose semantics are basic to the language; 2) A convention for functional abstraction, or the definition of new functions by means of expressions containing variables. The pure lambda calculus of Church[i] is illustrative of languages using only the abstraction mechanism; the combinatory calculus of Curry[12] exemplifies the use of primitives without abstraction. Curry[12] has demonstrated the equivalence of these mechanisms, with minor qualifications, and the choice between them for our purposes is largely a matter of c ante riierttf©; we provide here syntactic constructs for both. Beyond these constraints, the syntactic details of the languages discussed here are not important. A LISP-like syntax has been chosen, for the development of the models and to provide a definite basis for examples and illustrations, although the results and examples %ay be translated to conform to other syntactic conventions which are consistent with these constraints. Syntactic characteristics of our model languages include: 1) A finite alphabet including the alphanumeric characters and the special characters "(" and ")"; -16- 2.1 2) A countably infinite set of identifiers , eanh a finite string of alphanumeric characters of which the first is alphabetic; 3) A set of numeric constant*, each represented in the language by a finite string of digits* The elements of the model applicative languages are the applicative expressions (A£'s) whose syntax is given by: <AE> <identifier> <combination> <AE list> <lambda expression> <bvl> <number> <letter> <digit> := <identifier> | <number> ! <combination> | <lambda expression> :» <letter> ! <identifier><di#it> ! <identifier> <letter> = ( <AE list> ) = <AE> ! <AE> <spac«> <AE list> = ( LAMBDA (<bvl>) <AE>) = <null> i <identifier> <space> <bvl> = <digit> ! <digit> <nuaber> = A i B i . . . i Z = 1 i 2 ! ... ! o We assume of these model languages that data is eitfcar numeric or functional, that is, that the value computed for any applicative expression must be either a natural number or a function. 1 An expression X is atomic if X is an identifier or a number; in addition the following syntactic forms have special meaning in our model languages: 1) The syntactic form of a lambda expression is (LAMBDACa, a_ ... a ) b) i c n «„9S£ lt£i s i? n t0 i 8 nore u f o r the present other common data types (floating po i n L?V mbers ' arravs » character strings, lists) is Justified by their Sa^ ™v L a L?!i™5fri„ s 2w£ hat our r esul £ s concerning processing of numeric data may be extended to the processing of these other data as well. 2.1 -17- where LAMBDA is a reserved identifier in the language, the a are identifiers on the bound variable list of the lambda expressions, and the expression bis the body of the lambda expression. 2) The syntactic form of the application of the procedure (function) f to arguments x. ... x is (f x, . . . x ) i n Here f is presumed to be the representation of a functional datum, and the x are representations of arbitrary data which are supplied to the function f as arguments . There is in each language a small finite set of reserved identifiers used to denote primitive functions. Our initial models will include the following primitive function identifiers: 1) The logic values T and F, primitive functions defined such that the value of the application (Tab) is the value of the expression a., regardless of whether the value of the expression £, is defined. Similarly, the, value of (F a b) is the value of the expression & whether or not a. has a value. 2) The function PLUS of 2 arguments, defined such that the value of the expression (PLUS a b) is the sum of the values of the expressions a. and St. Tbe value of the application of PLUS is undefined if either of the values of a. or b_ is nonnumeric. 3) The function GREATER of 2 arguments, defined such that the value of the expression (GREATER a b) -18- 2.1 is the primitive function T if i has a higher numeric value than the expression b_, and F if the value of a_ is less than or equal to the value of b. We shall often refer to an identifier which is not a primitive function symbol as a variable . An occurrence of the variable y_ in the expression X will be termed a free occurrence if one of the following applies: 1) X is identically the variable y; or 2) X is of the form (A, ... A ) and the occurrence of y is free in one of in the A ; or 3) X is of the form (LAMBDA(a ... a.)M), y does not occur in the bound variable list (a. ... a ), and the occurrence of y is free in M. An occurrence of the variable y which is not free is b^und.. 2.2: Curried Functions The syntactic provision made here for functions of multiple arguments requires certain further elaboration. We may reasonably demand, for example, the ability to express the function MPLUS defined such that the value of tMPLUS m ) is the m-ary function which returns the sum of its m arguments. Such functions are, in general, unrepresentable unless some primitive mechanism is provided within the language for the abstraction of multiple argument functions. We might consider, the abstraction primitive ALPHA, defined such that the value (ALPHA F G m) is the m-ary lambda expression (LAMBDA(X 1 ...X )(G X m (F X, ... X .))) 1 m m l ra—i where F and G are presumed to represent (m-D-ary And binary functions, respectively. We might then define MPLUS so thj*t (MPLUS 2) returns PLUS, and (MPLUS n) returns (ALPHA (MPLUS n-1 ) PLUS n) for n>2. Such a primitive is, however, unnecessary in most languages. The technique of Curried functions may be used to couch multiple-argument functions in terms named in honor of H. B. Curry who developed this technique; see [12] 2 ' 2 -19- of unary functions, whence the application of F to arguments A A ...A becomes n ( ... ((F A ) A.) ... A ) 1 «... n and the n-ary lambda expression (LAMBDAU, A.,. . .A^>M* becomes (LAMBDA (A ) (LAMBDA (A 2 ) (LAMBDA (A n )M) ... )) The convention of Curried factions simplifies the presentation of proofs and interpreters, as only single argument Amotions need fee ^natdered; m therefore hastily adopt it for our present, purposes. Tfce conventional multiple argument syntax is slightly less complicatec| f bovver, and tends to greater clarity than the use of Curried function*; wft ^onaa^uently allow ourselves the informality of switching freely betwa«V *M two conventions at our convenience. We may then consider instances of t^ multiple argument syntax as an abbreviation for the corresponding Curried ^rntax, which we take as basic. An exception must be made in the first model language presented, however, as the FUNARG problem does not interact gracefully with Curried functions; hence in this case the assumption of single argument functions is not made. 2.3: The FUNARG Problem We are now in a position to give an example of a functional ly incomplete language, which we call S. S is an abstraction of the applicative subset of LISP and similar stack-oriented languages; it servea to introduce the notion of env4ronm . ent , and demonstrates that certain minimal structural constraints on environment handling mechanisms are necessary for t*e= expressibility of a particular class of functions. -20- 2.3.1 2.3.1: The S model An environment is a linear sequence of ordered pairs (or bindings ) (x,v), where x is an identifier and v is a value. Environments are thus a mechanism for the use of identifiers as variables, serving to record the values associated with each variable. We represent the environment which binds the variable X 1 to the value V , X to V , and so on, as ((x 1 ,v 1 )(x 2 ,v 2 ) ... ) The environment structure of the interpreter for S may be viewed as a stack, bindings being pushed onto the environment from the left at the start of the application of a lambda expression, and subsequently being popped from the environment at the completion of that application. The S interpreter finds the current value for a variable X by looking, in turn, at each binding starting with the leftmost; when a binding whose first element is X is encountered, the associated value (the second element of the binding) is taken as the value of X. We may describe this operation by defining a primitive function Iflfitaifi. of two arguments, corresponding respectively to the identifier to be evaluated and the environment in which its value is to be found: lookup[x;((X 1 ,V 1 )(X 2 ,V 2 )...(X n ,V n ))]= if xaX then V ; else lookup[x;((X 2 ,V 2 )...(X n ,V n ))] We now describe the interpreter for S as a function defined recursively as follows: S[x;e] = if x is a number, then x; if x is a member of {T,F, GREATER, PLUS} then x; if x is an identifier then lookup [x,e]; if x is a lambda expression then x; if x is of the form (T y z) then S[y;e]; if x is of the form (F y z) then S[z;e]; if x is of the form (GREATER y z) then: if S[y;e]>S[z;e] then T; else F; 2.3.1 -21- if x is of the form (PLUS y z) then S[y;e]+S[z;e] ; if x is of the form ( (LAMBDA(s, . ..s ) b) y,...y J where the in in s are identifiers, then S[b;(s 1 ,S[y 1 ;e])...(s n ,S[y ;e])e]; if x is of the form (y z. z_ ... z) where y is not a lambda i z n expression, then S[(S[y;e] z 1 ... z n );e]; else undefined Thus S[x;e] computes the value of the expression £ in the environment e_. S[x;0] (where is the empty envi ronmetifc$ computes the value of it on an S evaluator in its initial "bare" state; we may refer to this simpley as the JS xalus. o£ £. 2.3.2: Arithmetic Completeness of S We refer to a language as arithmetically complete if every computable first order 1 function is representable as a procedure of that language, ire show that S is arithmetically complete by showing that for every first order* partial recursive (hence computable) function there is a corresponding function in S. The constructions of this section are adaptations 'or those appear*** in DertouK>a£3] and are included >.fc«jBt«irfcpi$& far aalce of illustration; while each subsequent medal language 4a; vplso arithmetically complete, similar constructions apply in eaoh case and will not be repeated. As a preliminary step, we consider the S function given by: (LAr«DA(X ¥) ((LAMBDAU Y D)(D X Y)) X Y (LAMBDA (X Y) ((GREATER X Y) (PLUS 1 (»-* <MJ« 1 Y)H 0)) )) which computes the "recursive difference" function 1 Following the terminology of. logic, m ; &pPi*$*?M^™ * e ££?i?ri ?ft y numbers in its range and domain, and /^bi^M^jOpdar j pay contain (in addition to numbers) functions of order less than J. _22- 2.3.2 D[x;y] = if x>y then x-y else 0; by the algorithm D[x;y] = if x>y then 1+Dtx;y+1]; else 0; Note that the extra two layers of LAMBDA bi*d*n« aerve only to bind the free occurrence of the identifier D within its own deCAnltiPP, and thus to make the recursive function operate properly on S. We may define the pr ed ecessor function P[x] = if x<1 then else x-1 ; in S by the expression: (LAMBDA(X)(D XI)) where D is the recursive difference function defined above. Now we shall demonstrate that every partial recursive function of first order is representable as a, function in S. In the following, lower case letters represent partial recursive functions while upper case letters denote their corresponding S functions: 1) For every pair of «a««l»al numbers n and m, the m-argument oflaatftQt function of va fiie mi* expp •••id in &'*8^ (LAMBDA(X. ... X ) n) ■ m 2) For every pair of numbers n and m, the m-ary pro lection function which returns the value of its nth argument is expressed 4* S by: (LAMBDA(X r ...|y. X„> 3) The successor function i» expressed i^S by: (LAMBDA (X) (PLUS 1 X) ) 1 This is one of several "tricks" which may be used to perform recursion on S. The necessity of auch~ tricks, atema fri«JtM^S«^^fiyj|^^e|uacy of^S: the jf sf ilsJSf 8S^ oP^|- il^fe itl^^S&^^iyS^*^^ tiS^fo i *P*" a-generai discussion 2 « 3 ' 2 -23- «> (fiSUSaUlfia) For every choice of numbers n and m, m - ary partial recursive functions a o a ~> "ons gl ... g n> and n _ ary function f> fche m _ a functior defined by h[x ;x ;...;x ] = f[ a [x * 1 - r n 12 m 1L8 i LX r*' x m J » ... ,g n [x r ..x m ]] is expressed in S as (LAMBDAU. ... X )(F 1 ID (G, X 1 ... X m ) ••• (G n X 1 ••• V » where F, G, ... G n are the S expressions corresponding to f and g « respectively. 6 r'- 8 n' 5) (ttlUlla rsfiuxslaa) If the n-ary partial recursive function g and the (n*2)-ary primitive recursive function f are expressible in S as G and F respectively, then the (n+1 )-ary function h defined by: h[x 1 ,...x n ,0] = g[x r ...x n ] h[X 1 V^ * ««, X n .y.hCx 1f ...,x n ,y]] may be expressed in S by (LAMBDA (X 1 ... X n Y) ((UMBDACX^... X n Y H)(H Xl ... X n Y)) Xl ... X n Y (LAMBDA (X 1 ... X n Y) ( (GREATER Y 0) (F X 1 ... x n (P Y) (MX, ... X R (P Y))) (G X 1 ... X n ) )) )) where P is the representation of the predecessor function given earlier. 6) (iSlizCScjiEslaa) If the (n+1)-ary io^ recursive function h is expressible in S by H, then the partial recursive function g defined by g[x 1 ;...;x n ] = the Igaat y for which htx 1 ;...x n ;y] = is represented in S by _24- 2 .3. 2 (LAMBDA (X, ... X ) i ■■ n ( (LAMBDA (R)(R 0)) (LAMBDA (Y) ((GREATER (H X 1 ...X Y) 0) (R (PLUS 1 Y)) Y)) )) Finally, we note that the class of recursive functions is by definition exactly that class of functions obtainable through finitely many applications of the above six rules; hence the S representations given in the rules constitute a technique for constructing an S expression which represents any function which can be shown to be partial recursive. 2.3.3: Functional Incompleteness of S Recall that the functional completeness of a language L requires that every computable function defined on the semantic domain of L be expressible in L. Since the natural numbers and (by the preceding section) first order functions are included in the semantic domain of S, every second order function is definable on the domain of S. The functional incompleteness of S may then be demonstrated by showing that a simple second order function is not expressible as an S function. We begin by observing that a^e,*igher order functions aj^. expressible in S, e.g. the function g, (the "twice" Function} given by g[f;x] = f[f[x]J is expressible in S as (LAMBDA(F X)(F (F X))) hence it cannot be argued that ojUy. first order functions are expressible in S. The weakness in S which we will demonstrate Involves the inexpressibility of certain second order functions, notably f unctions which contain free variables and which appear as arguments or values (i.e., bodies) of lambda expressions: the so called FUHARG problem, 1 earlv e SLril^2 e Sfth f i^ FUHARG problem (as well as its name) arose from Dertculosf!}]? discussion see weizenbaum[23], Moses[10] or 2.3.3 _ 25 . Consider the unary function f, whose domain contains only integers and whose range contains only first order functions, defined by f[x] a that function g defined by g[y] = x+y The function f is computable; it may in fact be expressed in the lambda calculus by (LAMBDA (X> (LAMBDA (¥) (PLUS X YJ)) To show that £ is flat expressible in the language of S, the following definition is useful: r Defn 2.1: We say that the expression a. appears as a subexpression of the expression £. if any of the Fol*0wii$ n a1% 'tru*: 1) The expressions a. and tare identical; 2) b_ is of the form where a. appears as a subexpression of one or more of the b.; 3) b. is of the form (LAMBDAiX, .,.X JB) where a. appears as a subexpression of B. We say informally that b_ fioj&aina A if A appears as a subexpression of £. The basis of the inexpreasibilUy of X in § is eat^^^i* 4^ the proof of Lemma 2.2: Let A be any applicative expression and lejt B be a lambda expression appearing neither as a subexpression, of A nor in the environment e.. Then B does not appear as ^ subexpression of SlA;e]. PX2a£ is by induction on the recursion depth of sr*;ej. haaiS. For the following syntactic classes of A, the f computation of S[A;e] involves no recursion: Case 1: A is a number, a primitive function identifier, or a lambda expression. Then S[A;e]=A, and the lemma is trivially satisfied as -26- 2.3-3 B is not a subexpression of A. Case 2: A is an identifier other than a primitive function symbol. Then S[A;e] is lookup[A;e] which cannot contain B since by assumption the environment e does not contain B. j-nducUpn ; The remaining cases of the syntax of A follow; for these we assume that the Lemma holds for recursive calls to S. Case 3: A is an application of GREATER or PLUS; the* the value of S[A;e] is a number or logic value and does not contain B. Case 4: A is the application of a logic value T or F to arguments A., and A 2 « Neither A 1 nor A ? can contain B since A does not contain B; hence the inductive hypothesis applies tq #ither of the computations StA^e] and S[A 2 ;e] and B cannot appear in SC A; e] which is one of these values. Case 5: A is the application of a lambda expression (LAMBDA ( X, . ..X )M) to I n the arguments A r ..A n . By the inductive hypothesis, B does not appear in any of the values StA^e]. ..SfA n ;e], hence the new environment e'=(X 1 ,S[A 1 ;e]). . .(X n ,S[A B ;e] )e does not contain B. As a subexpression of A, M cannot contain B; thus the inductive hypothesis applies to the value S[M;e'] returned as the value of S[A;e]. Case 6: A is the application of Y to the arguments A,... A , where Y is I n* neither a lambda expression nor a primitive function symbol. Y is a subexpression of A and by assumption does not contain B as a subexpression. Then the inductive hypothesis applies to the computation of S[Y;e]=Y', and Y* does not contain B; a second application of the inductive hypothesis reveals that B cannot appear as a subexpression of S[(Y' A.,. ..A n );eJaS[A;e]. These cases are exhaustive, completing the proof. We can now characterize a major weakness of the language S by 2.3.3 -27- Thm 2.3: Every function expressible in S whose domain contains only numbers may have at most finitely many functions in its range. Proof : Functional values in S must be either primitive function identifiers or lambda expressions. As there are finitely many primitive functions, we need only show that each function of numbers in S has finitely many lambda expressions in its range. Implicit in this argument is the fact that the number of functions expressed by a Set of lambda expressions is no greater than the number of lambda expressions in the set. Each lambda expression which contains no non trivial occurrences of free variables represents (though not necessarily uniquely) a single function; lambda expressions with nontri vial occurrences of free variables (i.e., which compute different functions in differing contexts) do not correspond semantic ally to functions. By lemma 2.2, a function of integers can have lambda expressions in its range only if they appear as subexpressions of .the function, since for any integer n. and expression £ the expression (£. n.) can contain the lambda expression g. as a subexpression only if a; is a subexpression of £. As the function must be represented by a finite expression in the language S, it may contain only finitely many lambda expressions as subexpressions and hence has finitely many lambda expressions in its range. Clearly, the function £. defined at the beginning of this section is a function of integers having infinitely many functions in it»«*aage; we conclude that f_ is not expressible in S. The problem may be characterised as inadequate handling by S of lambda expressions containing free variables. It is apparent that free variables are evaluated in the environment in which a function is applied, rather than the environment in which it is evaluated. Thus lambda expressions with free variables have the property that the computation which they perform depends on values in the environment fef their caller; this dependency constitutes an implicit input and justifies our exclusion of such lambda expressions from the class of functions. Yet proper S functions may include such lambda expressions as subexpressions ; witness the S function -28- 2.3.3 (LAMBDA(X)((LAMBDA(Y)(PLUS X Y) ) 3)) >n:ch contains no free variables and hence no implicit inputs. The variable a., however, appears free in the lambda expression in its body; this innermost j.ambda expression is not a function. The question of the contribution of free variables to the functional richness of S naturally arises at this point: Are onere functions Which are expressible in S only through the use of free variables? Our suspicions lead to the conjecture that every function £ -vpressible in S may be represented by an expression F in which no lambda expression appearing as a subexpression contains free occurrences of variables. This conjecture does not completely deny the usefulness of free variables on the S machine. Indeed, lambda exppe*sion« with free variables are moderately well behaved when passed downward , i.e., as arguments to functions; under these circumstances, the principal danger is due to possible conflicts with variables bound by the functions to Which the lambda expressions are passed. They may, however, be considered to be "limited "unctions" with the qualification that they be applied within the scope of the ree variables in their original environment and that they may not be passed to functions whose bound variable list includes any of the free variables. V..ch qualifications seriously impair the semantic clarity of the language imposing them. 2.4: Evaluation Order ">.e functional incompleteness of S was shown to he related to the specific way :.n which S associates values with, variables in an interpreted program: i.e., he environment structure of S* The remaining s*e*l©ns &t this chapter resent model interpreters wit* alternative ernrironmem Structures, and which -;olve the specific problem demonstrated In Sj- however, they demonstrate similar inadequacies in the organisation of control structures r i.e. the data structure specifying whioh computations are to be performed and their relative 1 .-equence. Tne notion of control structure has never, to the author s knowledge, been fcequately formalized, informally it is the bookkeeping mechanism necessary :o resolve algorithms into sequences of operations — e.g., the use of a stack o record the return points of calls to a recursive subroutine. The first model to be presented is T, similar to S except that its environment is structurally a tree rather than a Stack. It is argued that T and S share a deficiency which stems from their evaluation order , in particular, from their uniform evaluation of arguments regardless of blether the resulting values are essential to the computation. T is thus fundtionally incomplete due to evaluation order. The N model, discussed in section 2.5, is closely related to the normal order evaluation of the lambda calculus. It is superior to T in that every expression having a T value has an equivalent R value, while certain expressions have N values but not T values. » 2.4.1: The T Model The traditional solution of the environment problem of S involves a new "internal" representation of a function, oiaai&l' 1 !.' closure. A closure includes, in addition to the information in a lambda expression, a specification of the environment Jtp which lta f l^ea^ Yariablea e are £o be evaluated. As the closure mechanism may^jsequirs the retention of environment branches corresponding to fuQOtvign^l app^oj^i,^ /**qm t ,,whicb -control haa^heen returned, the envirojwent becomes m i£S& either than f ,^he. M«jm»* &&&.<* S; hence we call our new language T. The di^i|anee b»tw,e«n T and S is that in T, the lambda expression (LAMBDA (a,... a.) b) in is no longer self evaluating. Its valua, lnenyl^nment a., is (FUNAHG(s 1 ...s ) b e) i n which is the representation of a closure in T. We define T as follows: T[x;e] = i^ xis^ a number,, then x; if x is a member of 4T,*,j3§«Tj^fcysi then x; if * is *f» identifier t*en lookup* xjei » 1 We say an expression X is self evaluating if the value of X is X. -30- 2.4.1 if x is of the form (T y z) then T[y;e]; if x is of the form (F y z) then T[z;e]; if x is of the form (GR EAT St y z) then: if T[y;e]>T[zje] then T; else F; if x is of the form (PLUS y z) then T[y;e)+T[z;e]; if x is of the form (LAMK)A(s 1 ...s„) b) then i n (FUNARG( Sl ...s J b e); if x is of the form ((FUNAHG(s 1 ...s n ) be^ y r ..y n ) then T[b;(s 1t Y[yi;e]) ... (s^Tty^eD+e^ ; if x is of the form (y z^ z ... z ) where y is not a FUNARG closure, then Tt(T[y;e3 z t ... z n >;e]; else undefined; We note that a lambda expression is not applied directly; it is first converted to a closure (by its evaluation), and then applied by the evaluation of its body in an environment formed by appending the bindings of its bound variable list to the closure environment. Thus the free variables of a lambda expression are evaluated in the environment in which the lambda expression is evaluated. The reader may verify that the function represented in the lambda calculus by (LAMBDA(X)(LAMBDA(Y)(PLUS X Y))) which the preceding section showed to be inexpressible in S, is expressible in T (indeed, by the same lambda expression). 2.4.2: Functional Incompleteness of T Except for the special cases involving the application of 1 the primitives T and F, the T evaluator uniformly evaluates the expressions supplied to an operator as arguments before the operator is applied. This order 1 ©f evaluation, which has been termed applicative order , has the virtue that each subexpression of 2.U.2 -31- an AE is evaluated at moat once, whereas in the normal order evaluation of the lambda calculus an argument to a function may be evaluated many times. The disadvantage of applicative order evaluation is that r arguments may be evaluated (once) even though their value is irrelevant to the computation; this is not merely a matter of occasional inefficiency, since the irrelevant argument may not be defined whereby the entire computation diverges. Consider the case of the trinary pro lection function P 31 [x;y;z]=x which returns its first argument regardless of whether its remaining arguments have defined values. The applicative-order counterpart of P is represented in T by the expression: f 31 =(LAMBDA(X Y Z> X) This expression does not return a value under ^-evaluation unless all three arguments have defined values. Our decision to distinguish between P_^ and f_. in effect recognizes the undefined, element. », as a member of the functional domains of our applicative languages. Intuitively, • represents the "value" of those computations which do not terminate, and whose expressibility in each language L is guaranteed by the Turing universality of L. We now show that P . is not expressible in T; Thm 2.4: For every AE £, the T value of the expression (I 3 • •) [2.5] (where * denotes any expression whose T value is undefined) is undefined. Proof: We consider exhaustively the possible I values of the operator £: If £ is a number or a primitive operator, then the value of [2.5] is undefined due to an error in functional ity, i.e. the application of a primitive to arguments for which it is not defined, may assume that f is either a combination or a lambda expression, in which cases the value of the combination is the value of the application of the T value of f to the specified arguments. If the value of £ is a number or a primitive, _32- 2.4.2 [2.5] is again undefined due to an error in functionality. Hence the value of f_ must be a closure. The computation of the application of a closure involves binding the values of eaern argument onto the environment, hence the evaluation of [2.5] entails evaluation of each argument. Since not every argument has a defined T value, the value of [2.5] is undefined. Since clearly the projection P . has the property of £ in Theorem 2.4, T must te functionally incomplete if we are to consider P a function. 31 2.5: The N model This section introduces an applicative language whose interpretation involves normal order evaluation. The superiority of N over T derives from this revised evaluation order of N, which permits an expression t° be evaluated even though subexpressions of it may be undefined. A theorem of Church and Rosser establishes that if an AE, A, has a value under iaSL evaluation order, then it has that value under normal order evaluation; thus in terms of evaluation order, M is optimal. The simplest implementations of normal order evaluation involve the substitution of argument text in the bodies of lambda expressions, rather than the binding of argument values in environments. While the explication (and implementation) of such substitution algorithms is relatively straightforward, evaluation by simple substitution is often inefficient since 1) It involves making many copies of program text during execution, and 2) It often involves multiple evaluations of the same subexpression. for reasons of efficiency, substitution evaluators are thus primarily of theoretical interest. More efficient implementations of normal order evaluation retain the environment structure of the T model, and introduce additional mechanism to indicate which bound expressions have or have not been evaluated. Since the environment implementations of normal order evaluation involve considerable 2.5 -33- bookkeeping machinery and are hence conceptually much more complex than the substitution algorithms, they will not be pursued. 2.5.1: Axioms for the Lambda Calculus The primordial applicative language is the lambda calculus, which has been the subject of much investigation since its conception by Alonzo Church in the 1930s. The semantic basis of the lambda calculus is a set of axioms which define an equivalence relation, =, on expressions of the language. Each axiom may be interpreted as a conversion rule for reduction rule ) in the sense that it provides a means for converting (or reducing) an AE to an equivalent (uqder = ) AE having a different form. The presentation of the axioms in this chapter is somewhat informal, serving primarily as motivation for the N interpreter; the interested reader is referred to Curry[12] and Hindley[21] for further detail. Related issues are also covered in greater depth in later chapters of this report. The axioms of the lambda calculus are of 4 types, designated alpha (equivalence under renaming), beJA (function application), delta (primitive function definition), and, in some formulations, ejfcfi. The delta and eta axioms are not used in all formulations. The eta axiom seems to serve no important function in the evaluation of expressions and will be presented here only in passing. The delta axioms may be avoided by well known coding techniques which involve the representation of nonfunctional data, e.g. natural numbers, as lambda expressions. The formulation which will be primarily referred to in subsequent chapters comprises the alpha, beta, and delta axioms, and is often termed the beta-dej.ta- cal cuius in the literature. Unless otherwise qualified, generic references to "the lambda calculus" in this report, denote the beta-delta calculus. The equivalence relation s of inter convert ability is generated by a relation Many such codings are possible: a popular choice represents by the expression (LAMBDA (X) (LAMBDA (Y)Y) ) and the number n+1 by (LAMBDA (X) (LAMBDA (Y)((N X)(X Y)))) where N is the representation of the number n. For development of such a coding, see Church[1]. -3M- 2.5.1 -> of reducibilitv : hence X->Y implies X=Y which, in turn, implies Y=X. Reducibility is in general antisymmetric, however; thus -> provides an ordering of equivalent expressions which has important ramifications in the lambda calculus. The relation -> is defined to be a monotone relation meaning that it has the following properties: Reflexivity: For every X, X->X; Transitivity: If X->Y and Y->Z, then X->Z; Monotonicity: If X->Y and B is the result of substituting, in an expression A, X for an occurrence of Y, then B->A. The relation = is in addition an equivalence relation; hence X*Y implies Y=X. Central to the axioms is the substitution rule . S, of fundamental importance to the lambda calculus as well as the theories of the following chapters of this report. S is formulated as a three argument function, such that the meaning of S[X;Y;Z] is roughly "the result of substituting the expression X for free occurrences of the variable Y in the expression Z. The definition of S is further complicated, however, by the requirement that the operation S[X;Y;Z] not introduce conflicts between free variables in the expression X and bindings of X within Z. There is a long history iof incorrect algoritms for S; the definition given here is due to Curry: Defn 2.6: For expressions X and Z, and variable Y, the expression S[X;Y;Z] is defined as follows: 1) If Z^Y, then X; 2) If Z is a primitive, number, or identifier other than Y, then Z; 3) If Z is of the form (Z 1 Z £ ) then (SCXtfjZ,} S[X;Y*;Z g ]); 4) If Z is of the form (LAMBDA(A)M) where Y=A, then Z; 5) If Z is of the form (LAMfiDA(A)M) where ¥ is different from A, then (UMBDA(B)S[X;Y;S[B;A;M1T). where the variable B is chosen as follows: i) If Y does not occur free in M or if A is not free in X, then B=A; ii) Else B is any variable which ooeurs free neither in M nor in X. 1 Terminology after Curry[12] 2.5.1 -35- We now procede to the statement of the axioms: Axiom alpha : If E is a lambda expression of the form (LAMBDA(X)M) and the variable Y does not occur free in K, thftfi £^jLAl|HM<X>S{Y;X;M]). We say that expressions A and B are co rurruept if A can be converted to B by alpha conversion alone. No^te that if , X->Y by alpha conversion then Y->X by alpha conversion; hence X=Y. Congruence is thus symmetric and transitive, and under most circumstances congruent expressions may be treated as identical* We say that expression X Is in normal form if the only reduction which can be performed on X is alpha conversion. Axiom beta : If E is an, expression of,,the fora ( £UH8pA(X)M) A) then E->S[A;X;M], ..,,. Axiom fila: If E is an expression of the form (LAMBDA(X)(M XJ) where X does not appear free in M and M is a lambda expression, then E->H. Axiom delta : If E is an expression of the form (F A, A '... A ) where F is a i e. n primitive function symbol and each Ai is in normal form and contains no free variables, then E->f[A,;. ..;A J where t Is the operation denoted by 1 n F. The following two theorems are of fundamental importance in the lambda calculus. The first is dbe, in its Initial primitive form, to Church and Rosser and is referred to in the literature as the Church-Rosser Theorem: Thm 2.7: Let X and Y be expressions such that XxY. Then there exists an expreslon, 2-, such that X->Z and Y->Z. proof may be found in Curry[12] or HindleyC21] and elsewhere. The Church-Rosser Theorem shows that the lambda calculus is consistent in the sense that the relation = is nontrivial; in particular, X=Y is not true for incongruent expressions X and Y in normal form. We can thus prove that expressions X and Y are not interconvertible by finding normal forms X' and This definition is recast more formally in the terminology of Chapter 4. -36- 2.5.1 Y , where X->X' and Y->Y', which are incongruent. Unfortunately, not every expression X is convertable to an expression X' in normal form. For example, the important expression Y= (LAMBDA (F)( (LAMBDA (H)(F (H H) }>(LAMBDA(H) (F (H H))))) which is the "paradoxical combinator" of Curry, has no normal form. Further discussion in this area follows in Chapters 1 and 5, along with related technical developments. A second important theorem, due to Corrado Boehm, has, been proved only for systems which prohibit delta conversions: Thm 2.8: Let X and Y be incongruent expressions in normal form, and let C and D be arbitrary expressions. Then there exists and expression Z such that C=(Z X) and D?(Z Y). Proof originally appeared in Boehm[20], in Italian; a proof in English appears in Curry[27]. Boehm's Theorem guarantees that incongruent normal forms, in the beta- eta calculus are semantically distinct; in particular, the axiomatic assertion that any two incongruent normal forms are interconvertible results in an inconsistency. The extension of Boehm's Theorem to systems, which include delta conversions requires that the constants added to the pure lambda calculus also be semantically distinct. We might, for example, formulate a calculus including the numeric constants without providing any means for distinguishing between them: we could provide the primitive PLUS but not GREATER. While this formulation is valid in terms of the lambda calculus, Boehm's Theorem is clearly inapplicable since there is no expression Z which distinguishes, say, between the normal forms 2 and 3. 1 deltI'conve l rsio , S" lati0n lncludin « axioms al P na . bet *. and eta, but excluding 2.5.2 -37- 2.5.2: Normal order: Substitution Each of the lambda calculus axioms provides a means by which an applicative expression E may be reduced to an equivalent expression E'. While the axioms themselves place certain restrictions on the order in which such reductions may be performed, 1 the evaluator of an applicative expression has a great deal of freedom to choose the order in which to evaluate subexpressions. Normal order evaluation specifies that at each evaluation stage, the leftmost reducible subexpression is to be converted. 2.5.2.1: The N Evaluator We define the N value of an AE x as follows: N[x] = if x is a number, then x; if x is a member of {PLUS, GREATER} then x; if x is a lambda expression, then x; if x is of the form (PLUS a b) where N[a] and N[b] are both defined and numeric, then N[a]4N[bJ; if x is of the form (GREATER a b ) where N[a] and N[b] are both defined and numeric, then if N[a]>N[b_] then (LAMBDA (X Y)X) else (LAMBDA(X Y)Y) ; if x is of the form ( (LAMBDA (a) b)c_) where a is an identifier and band c are AE's, then N[b'] where b' is the result of substituting c. for each free occurrence of a in Jb; if x is of the form (a b) where a and b are AE's and a. is not a lambda expression, then N[(N[a] b)]; else undefined; Note that we have eliminated the primitives T and F, which are entirely equivalent in N to the lambda expressions which replace them as values of GREATER. OY ^f ^ e x P ress i on .E containing applications of lambda expressions, for example, is beta-reducible. Applications ofaxiom alpha, ie the renaming of variables, may be required before axiom beta is applicable! renami ng °r -38- 2.5.2.2 2.5.2.2: Axiomatic Consistency of N We show in this section that N evaluation is consistent with the semantics of the lambda calculus by demonstrating that N preserves the equivalence relation Thm 2.9: Let E be any AE such that H[E] is defined. Then E->N[E] where -> is the reducibility relation defined by the lambda calculus axioms. proof : by induction on the level of recursion in the computation of N[EJ. basis : if E is a number, a primitive, or a lambda expression then N[E].=E. induction : we assume that the Theorem holds for recursive calls to N. Then the Theorem holds for the remaining syntactic cases of E by the monotonicity of ->. We note in passing that H[E] is not necessarily a normal form. Lambda expressions, in particular, are not reduced by H r since otherwise the evaluation of certain meaningful expressions (e,g. the paradoxical combinator Y) would not terminate. 2.6: Functional Domain of N In this section it is shown that the entire domain of N constitutes a functional domain satisfying the intuitive criteria of [1.1]. We interpret the semantic equivalence relation, ", on the domain of N as follows: For X,Y in D N , X~Y if and only if [2.10] for every Z in D and number n f (Z X)=n <=> (Z Y)*n where D is the domain of N* We now justify this interpretation of " on N N thru Thm 2.11: The domain of H is a functional domain, obeying the criteria of [1.1], under the above interpretation of ". proof : The equivalence relation ~ defined in [2.10] must be shown to obey 2.6 _39- the three clauses of [1.1] over the domain D„ of N. We treat the clauses N individually: 1) For numeric constants X and Y, we must show that X"Y <=> X=Y. <=: direct, by the equivalence of identical expressions. =>: Assume X~Y. Then by beta-reduction, ((LAMBDA(a)a) X)=X and ((LAMBDA(a)a) Y)=Y and thus, by [2.10], X=Y since they are numeric. By [2.7] there exists a Z such that X and Y are each reducible to Z; since X and Y are not reducible, Y, Y, and Z must be identical. 3) To show: X~Y <=> for all Z in D , (Z X)~(Z Y) or neither defined. =>: Assume false. Then for some X~Y there exists a Z such that (z 1 X)T(Z 1 Y) where | is the negative of ~. This implies, by [2.10], that there exists a Z_ such that (Z 2 (Z 1 X))=n for some numeric constant n but not (Z 2 (Z 1 X))=n (we are assuming here one of two completely symmetric cases with no loss of generality - the other case follows by interchanging the symbols X and Y). Defining Z by the lambda expression we note that hence by [2.10] X|Y. Z 3 =.( LAMBDA (a )(Z 2 (Z, a))) (Z X)=n but (Z Y)*n -40- 2.6 <=: Assume that for all Z in D , (Z X)~(Z Y). Then (Z X)=n (for numeric constant n) if and only if (Z Y)=n by the argument of part (1). Hence by [2.10] X~Y. 2) It must be shown that X~Y if and only if for all Z in D N , (X Z)~(Y Z). From part (2) of this proof, X~Y <=> for all Z: ((LAMBDA(a)U Z)) X)~( (LAMBDA(a) (a Z)) Y) hence, by beta-reduction, (X Z)~(Y Z) The significance of Theorem 2.11 is that every element of the domain of N corresponds to some element of the abstract semantic domain: every element of D. T is intuitively functional. Thus N (and the lambda calculus on which it is N based) is a language of "pure" functions. We shall find in the next chapter that this pleasant property costs us something, however, in terms of ex pr es s ive powe r . 2.7: Summary The material in this chapter is largely introductory. The three interpreters presented are abstracted from conventional implementations, and their scrutiny serves to relate common implementation issues to the expressibility of functions. The major findings were: 1) Each language is arithmetically complete, in the sense that every computable function defined on the natural numbers is expressible. 2) The FUNARG problem leads to the inexpressibility in S of functions whose domain contains integers and whose range contains infinitely many functions. 3) Applicative order evaluation renders inexpressible in T every function whose domain includes *, the undefined computation. An example of such a function is the constant function (LAMBDA(X)3) of one argument. 2.7 -41- 4) The interpreter N, based on the normal order evaluation of expressions by substitution, suffers from neither of these deficiencies. We can construct a functional domain F such that every expression X in the domain of the language N corresponds to an element of F; thus N is a "pure" language in the sense that every expression corresponds to a function or a number. This is not true, for example, in S, where lambda expressions containing free variables can compute different functions in varying contexts. We are left with N, an interpreter whose behavior is intended to model the lambda calculus; the remainder of this report, roughly speaking, deals with a particular weakness common to N and the lambda calculus. This empty page was substituted for a blank page in the original document. 3 -4 3- Chapter 3: Motivation for a Multi-valued Semantics Central to this chapter is the argument that the N model, and hence the lambda calculus, is functionally incomplete because of the inexpressibility in N of a class of computable functions on N's domain. The inadequacies of N leading to this weakness are explored, and two new model languages are presented, each curing the problem in a different manner. The first model, which has provision for encoding representations of functions as integers, is found to be unsatisfactory for both practical and semantic reasons. The alternative solution proposed in this chapter involves mechanism for the representation of semantic elements with multiple values; this mechanism, called EITHER, is the principal focus of the remainder of the Thesis. 3.1: Necessity of non-functions: WHICHFF Consider the family of partial functions, {FF. } for i ranging over N, which satisfy the following conditions: for each natural number i., FF 1 Ex] = i, i=x [3.1] divergent, i^x Thus each FF has a single element in its domain: the number i. For any other argument the value of FF [x] is undefined. The {FF. } are clearly partial functions in the intuitive sense of Defn [1.1], and are computable in each of the model languages considered here. Furthermore, they are semantically distinct: for no numbers i*j does FF -FF.. There is then nothing intuitively objectionable about a function which maps each FF. to its corresponding i. Consider such a function WHICHFF which, for each natural number i., has the property that: WHICHFF[FF. ] = i [3.21 Intuitively WHICHFF is a function from {FF. } onto N; furthermore it is demonstrably computable using "dovetailing" or multiprocessing techniques. Note in particular that the following definition of WHICHFF satisfies the condition of [3.2] : -44- 3.1 WHICHFF[f] = i such that f[i3=i, C3-33 if such a number i exists; else undefined We may view the dovetailed evaluation of WHICHFF£f] as the computation of f[0] for one second, the computations of f[0] and f[1] each for two seconds, and similarly until any one of the computations f£i] terminates normally; the value of this f[i] would then be taken as the value of WHICHFF[f]. However, WHICffiT is not expressible in N; this is a result of Thm 3.4: Let L be an arithmetically complete applicative language and let D be the domain of L. Then no function WHICHFF having the properties of £3.33 is functional over D^. proof by reduction to the halting problem. Assume that D, contains a function WHICHFF having the property given in £3.3]. Then for any function f in D, and any number 1, Lt (WHICHFF £)3"i if f_~FF i . How consider the union of the functions FF, and FF , given by: FF t2 £x] = 1 r L£x]=1; 13.5} 2, L[x]=2; divergent otherwise FF 1? is clearly a computable first order function, hence it is expressible in L by the arithmetic completeness of L. Now L[ (WHICHFF FF J] can have as its value at most one of {1,2}; thus either L[ (WHICHFF FF _)]*1 or L[ (WHICHFF FF )}#2. Assume, with no loss of generality, the former. Then define the second order function g. as follows: g[f] = the function g , where g f Ci] = 1, 1=1; 2, i=2 aM f£0] defined; divergent otherwise. For every computable first order function f, g. (or equivalently g£f]) is evidently computable. Moreover, if f [0] is undefined then g_ is identical to the function FF^; otherwise g_ is identical to the function FF We use the ability of WHICHFF to distinguish between FF 1 and FF 12 to determine whether f[0] is defined, by means of the function & given by 3-1 -45- h[f] = WHICHFF[g[f]] We note finally that for any function f f[0] convergent => g[f] - FF 12 => h[f]*1 ; and f[0] divergent => g[f]~FF => h[f]=1 Hence h[f]=1 if and only if f[o] is divergent. The divergence of f[0] is decidable, as one of the computations h[f] and f[0] must converge; thus the function h provides a solution to the "halting problem" for first order functions, and is a well known noncomputable function. Since h is clearly computable in terms of WHICHFF, we conclude that WHICHFF is not a computable function over any domain including the first order functions. Since it was shown in the last chapter that every function expressible in N is functional over all of the domain of N, it follows that WHICHFF is not expressible in N. This inexpressibility relates intuitively to two aspects of the implementation of the N interpreter: 1) The interpreter does not admit multiprocessing. If, in the evaluation of expression A, N embarks on the evaluation of a subexpression a of A whose N value is not defined, then the N value of A is not defined. 2) The only mechanism in N by which a function f can recover information about its functional argument g. is the application of g.. There is no means by which f can discover the algorithm (or program) by which g. computes values, even though the internal representation of g. necessarily includes this information. Hence if f is to make any use of g., then g. must be applied to some argument; By the constraint (1) above, the nontermi nation of this application results in the nontermi nation of the application of f. The correction of either of these deficiencies is straightforward in an implementational sense — many extant languages boast provisions for multiprocessing and/or access to representations of functions. However, neither "correction" is easily record i<>h , ,■,•<- v. *u~ ' Ict -°nciled with the semantics of an applicative language. The second limitation of N seems a natural consequence of our -46- 3.1 distinction between the notions of a function f and any of the algorithms for computing £ from its arguments; a language which provides mechanism for distinguishing between algorithms for computing a particular function f. would certainly have non-functional elements in its domain. The semantic ramifications of a cure to the first problem, however, are more subtle and will be explored in detail. The following sections present two alternative extensions to N, each corresponding to a "fix" of one of the above limitations. The function WHICHFF is expressible in each. 3.2: Coding primitives: The C model We noted that a limitation of N, justifiable by our intuitive respect for the semantics of functions, is that no information can be recovered about an N function without the application of that function. In particular, S provides no means for recovery of information about the representation of a function as an N expression. We have thus avoided the "Turing Machine tar pit" « the argument that any language as powerful as a Universal Turing Machine has exactly the same set of expressible functions. The C model presented here has, in addition to the primitives and structure of N, primitives for the translation of the representation of language elements to and from a tractable form. Making the fundamental assumption that any function defined on a domain F is computable if and only if it is computable from the representations of elements of F, we must conclude that a Universal Turing Machine (or its equivalent) operating on the representations of arguments to the computable function f can compute representations of the values of £. This is the substance of our claim of functional completeness of the language C. The interpreter for C is identical to the interpreter for N except for the addition of the primitive operators CODE and WECtfDE. CODE maps representations of the domain of C into the natural numbers: CODE: D c -> N 3.2 -47- and may be viewed as a Goedelization of the character string representing its argument. The claim we make for CODE is that if (CODE X) and (CODE Y) have the same (numeric) value then X and Y are semantically equivalent; they are in fact represented in an identical manner. We cannot, of course, claim that in general X~Y implies (CODE X)=(CODE Y), as there are many representations of each semantic element and the semantic equivalence of the representations is effectively undecidable. The operator DECODE is the inverse of CODE: given the Goedel number of the representation of an element, it returns the element. We thus claim that each expression X is semantically equivalent to (DECODE (CODE X)). Our claim for the functional completeness of C is formalized, to the extent possible, in Thm 3.6: Let F be a functional domain of C, and let g: F -> F be a computable function on F. Then g is expressible in C, i.e., there is an expression G in the domain of C such that for all x,y in F, g[x]=y implies that (G X)~Y. proof : Since g is computable then so is h defined by: h = (LAMBDA(Y)(CODE (g (DECODE Y)))) as it is simply the composition of computable functions. Furthermore, since h is a function from N to N, it is expressible in C by the arithmetic completeness of C; let H be the representation in C of h. Then the function g is expressible in C by: G _= (LAMBDA (X) (DECODE (H (CODE X)))) It must be recognised that CODE is not functional: it radically disobeys the intuitive requirements of Defn 1.1. We note, for example, that CODE might return different values for the arguments (LAMBDA(X)X) and (LAMBDA(Y)Y) as they have different representations, violating our requirement that semantically equivalent arguments produce semantically equivalent results. -48- 3.2 WHICHFF example of the preceding section. The representation of WHICHFF in C involves writing an interpreter, operating on the CODEd representations of C expressions, which simulates the required "dovetailing" by computing 1 step of (g 1), 2 steps of (g 2), 2 steps of (g 1), etc. Presentation of actual code for WHICHFF on C would be, at best, a messy task; it is hoped therefore that the reader will accept the expressibility of WHICHFF in C on the basis of Theorem 3.6 and this informal discussion. 3.2.1: The Turing -ma chine Tar Pit The introduction of the specter of coding requires further reflection. We have made the enticing observation that, with the introduction of a simple mechanism allowing the representations of functions to be accessible as data, every computable function becomes expressible. We have noted corollary disadvantages — (i) the semantic confusion resulting from the nonfunctional character of (DDE, and (ii) the practical absurdity of having to include the code for interpreters in the definitions of certain functions. However, the inclusion of coding primitives in an applicative language may be objected to on more fundamental grounds than the above. The stated semantic goal of an applicative language is the representation of functions. Thus such a language provides a set of rules and conventions for associating expressions with abstract functions; moreover, the power and consistency of the language stem largely from the applicability of these rules and conventions to every expression in the language. In the lambda calculus, for example, we are assured that expressions which are interconvertible via the alpha and beta axioms are equivalent. The cost of this assurance is a corresponding constraint on the computations which we might perform: the alpha axiom positively prohibits us from writing a function which distinguishes (LAMBDA(X)X) from (LAMBDA(Y)Y). We accept this constraint because the structure which it imposes is useful to us; we recognize that we cannot be assured of a relation and simultaneously be allowed to violate it at will. Coding primitives may be viewed as a mechanism for violating the structure imposed by an applicative language. None of the lambda calculus axioms, for example, are valid in the presence of coding, since "functions" can be written 3.2.1 -49- which distinguish between interconvertable expressions. The rules and conventions for representing functions are, in effect, abandoned. The programmer is thus freed from the structural constraints of the language, but finds himself in a semantic anarchy - while he may write any function he Pleases, he may make no assumptions about the structure or representation of its arguments. 3.2.2: Functionality of DECODE We may convincingly defend the contention that CODE is not a function by demonstrating that it returns semantically distinct integers, say, for the equivalent arguments (LAMBDA(X)X) and (LAMBDA(Y)Y). This demonstration does not apply, however, to the inverse of CODE; there is nothing inherently nonfunctional in the fact that DECODE returns semantically equivalent expressions (LAMBDA(X)X) and (LAMBDA(Y)Y) when given semantically distinct integers as arguments. It is the purpose of this section to demonstrate that functions with the property of DECODE (i.e. mapping a subset of the natural numbers onto the entire domain of discourse) are expressible in N and the lambda calculus. 3.2.2.1: LAMBDA-free AEs It is convenient for certain purposes to use the techniques developed primarily by Curry[12] of the calculus of combinatory for the reduction of applicative expressions to equivalent expressions whose use of lambda expressions is highly restricted. For our purposes we shall consider the combinators listed below (along with their respective definitions): I =. (LAMBDA (X)X) K =. (LAMBDA(X)(LAMBDA(Y)X)) W =. (LAMBDA (X) (LAMBDA (Y)(X Y))) S =. (LAMBDA(X) (LAMBDA (Y) (LAMBDA (Z)((X Z)(Y Z)))) G 1 =. (LAMBDA (G) (G G) ) G 2 = (LAMBDA (G) (LAMBDA (Y)(Y G))) G 3 =. (LAMBDA (Y) (LAMBDA (X)((Y X) X))) -50- 3.2.2.1 G u = (LAMBDA(G)(LAMBDA(D)(LAMBDA(X)(G (D X))))) We show in this section that every applicative expression using no lambda expressions other than the above combinators; we begin with Lemma 3.7: Let R be a LAMBDA free AE in the single argument applicative language L, and let R contain occurrences of the variable x. Then R is equivalent (by alpha and beta axioms) to a LAMBDA free AE of the form (R' x) where R' contains no occurrences of the variable x. proof is by structural induction on R. basis : R is atomic (in particular, R is not a combination). If r is the variable x, then r' is (I x)=x (by axiom beta). If £ is not the variable x_, then r. contains no free occurrences of & and r' is ((K r) x) = ((LAMBDA(X)r) x) = r. induction : R is a combination of the form (R. R 2 ). By inductive hypothesis, R=((R ' x)(R ' x) ) for some AEs R ' and.R ' not involving the variable x; then R'=(((S R 1 ) R g ) x) = ( (LAMBDA (X) (LAMBDA (X) ((R 1 X) (Y X))))) = ((R 1 x)(R 2 x)). The principal result of this section is the following adaptation from Curry's Synthetic Theory of Combinators: Thm 3.8: Let A be an AE in a single-argument applicative language L whose semantic equivalence obeys axioms alpha and beta. Then A is equivalent to a LAMBDA-free expression A* containing only the combinators I, K, W, S, G., G_, G,, Gh, and the primitives and constants of L. proof : We show that, given any such A which is not LAMBDA-free, we can construct an equivalent A' containing fewer LAMBDAS. Let a. be an innermost LAMBDA expression occurring as a subexpression of A. We then construct A' by replacing a as follows: Case 1: a. is of the form (LAMBDA(x)x) for some variable x; we replace a. by I (equivalent by axiom alpha). 3.2.2.1 -51- Case 2: a is of the form (LAMBDA(x)y) where x and y are different variables; we replace a, by (K y). Case 3: a is of the form (LAMBDA(x)(b x)) where x is a variable and b is an AE: replace a by (W b)=(LAMBDA(Y) (b Y) ) Case 4: a is of the form (LAMBDA (x)(c d)): By Lemma 3.7, the body (c d) is equivalent to an AE (r' x) where the variable x does not appear in r'. Then a=(LAMBDA(x) (r ' x) ) which is reducible according to case 3. Since each expression A which is not LAMBDA free is thus equivalent to an expression A' containing fewer LAMBDAS, a finite number of such reductions will reduce each such A to a LAMBDA free A*. This completes the proof. It is a relatively simple exercise to show in addition that each of the c xnbinators I, W, G^ G 2 , G_, G^ is in turn equivalent to an expression in K and S, allowing us to simplify Theorem 3.8 by eliminating all but 2 of the combinators. This is unnecessary for our purposes, however, so long as the number of combinators required is finite. An important observation to be made at this point is that the construction of A* detailed in Theorem 3.8 is ef fective ; thus we could program a computer to convert AEs to LAMBDA free form. 3.2.2.2,: An Enumeration of D„ N In this section it is demonstrated that the domain of every applicative language with the power of the N model contains functions which .enumerate the domain of that language, ie, each such language L with domain D contains a Li function f: N -> D such that for every finite expression x. in D there is a number n. which Li satisfies (f n)=x. We procede by Goedelizing the LAMBDA free expressions of V Let pair be a number pairing function such that, for each i and j in N, the value of pair[i,j] is a unique number P ±J , and let left and right be functions recovering the components of a pair; ie, for every i and j, left[pair[i, j]]=i and right[pair[i,j]]=j. There are many well known such pairing functions; since they are all first order computable functions, we may assume that they are expressible in each of our model languages. Let us now suppose that we label the (finitely »ny> primitives of the language L as p,, P 2 , ... P„. Note that we include the combinators K, I, 0,, etc in this list so that we can enumerate LAMBDA free expressions only. We now specify the coding details: for each LAMBDA free expression x, we define the Goedelization &[x] as follows: g[x] = if x is a number then pair[0;x); if x is a primitive p. then pair[1;j]; if x is a combination (a b) then pairleUbgEb] ]; The function * is computable from t*e representation of x, but we cannot in general claim that it is computable from the functional properties of x. The function k is, in fact, a satisfactory choice for the CODE function of the C ■od.1. assuming (as we may) that we are content to deal with LAMBDA free expressions of C. If such a function * could be shown to be computable in, for example, the N model, we would have a direct a. pxiori demonstration that the languages are expressively equivalent. We must, however, be content with the expressiblity of a semantic inverse of &: the function ejm defined such that, for every LAMBDA-free expression x_, enu[g[x]]=x. This apparent asymmetry can be explained by the observation that g. is not a function, in the sense of Defn [1.1] which prohibits the mapping of semantically equivalent expressions into differing numbers. The fact that ejm. may map different numbers into semantically equivalent values is consistent with its functionality. We label the expressibility of enu. as Thm 3 9: Let L be an extension of N with primitives 11, 12 In (including combinators K and S). Then there is a function enu_:N->D L such that, for every LAMBDA free expression x in D L , there is a number i such that enu[i]"x. 3.2.2.2 -53- proof is a straightforward programming job. Such a function for the language N would take the form: (LAMBDA(N) ((GREATER (LEFT N) 1) ((ENU (LEFT (RIGHT N))) (ENU (RIGHT (RIGHT N))) ) ((GREATER (LEFT N) 0) ((GREATER (RIGHT N) n-1 ) In 11)...)) (RIGHT N) ))))) where li is the ith primitive of N, and LEFT and RIGHT are the N expressions corresponding to the ^eft^ and r ^ ft fr functions above. 3.?: E model: Multiprocessing primitives An extension to the N interpreter which is somewhat more palatable than the use of coding primitives is the addition of mechanism for multiprocessing: the quasi-simultaneous evaluation of several expressions. We consider here the E model, which is the IN model of Chapter 2, augmented by the primitive operator EITHER whose interpretation is as follows: For every choice of expressions a. and b_, [3.10] E[ (EITHER ii)] « if E[aJ is defined but E[bJ is not, then E[gJ ; if E[bJ is defined but E[aJ is not, then E[b]; if E[aJ and E[b_] are both defined then one of these values; else undefined. Note that we do not specify which of the arguaents is- returned if both have defined values; we may consider that this selection iS made by some nondeterministic process over which we have no control. EITHER is evidently computable by dovetailing techniques, eg by evaluation of E[aJ and EfbJ each for 1 step, then each for 2 steos, and so on mnfcil one evaluation or the other returns a value. EITHER is not, however, functional: in the case where a and - 5 *- 3.3 b each have defined values (and their values differ), then the value of (EITHER a b) is dependent on the representation of a and band on details of scheduling of the dovetailed computation. The power of the ej^ex primitive is demonstrated by the expressibility of WHICHFF in E as follows: WHICHFFffJ = gl [f_; ] where g^hjfl] = eitherthjnjjg^hjn+l ] Note that for i>j, g^FF^i] is undefined and hence for i<j gl [FF.;i],j. Thus for every number j, E[ (WHICHFF FF )]=j. J The presentation of the EITHER primitive in this section is informal, based largely on its intuitive relation to the implementation mechanism of multiprocessing. The formalization of this mechanism is a principal topic of the remaining chapters. The remainder of the present chapter explores the impact of EITHER on the semantics of an applicative language. 3.4: The Intuitive Paradox The reader has doubtless noticed that fundamental questions raised in the first section of this chapter demand a more precise characterization of the hitherto vauge notion of functional completeness. Specifically, Theorem 3 4 shows that WHICHFF is not functional over the entity of *ny_ functional domain which includes all first order functions. Thus the basic intuitive requirements of [1.1] are inconsistent with the existence of a functional domain F which is arithmetically complete and tmludss every computable function f :F->F. Two alternatives facing us are the following: D We can deny that WHICHFF is a computable function. Indeed, Theorem 3.4 may be interpreted as a statement that no computable function defined on first order functions has the properties of WHieffTF given in [3.2] Our intuitive claim that WHICHFF is a computable fMctibn Is based on the incomplete specification of its behavior otcr -the entire functional domain: [ 3 .2] merely defines it over the restricted domain of {FF }. 3.*» -55- 2) We can revise the notion of a functional dqmain F such that, for every function £ in F there is a dojaaia o£ specification over whicW the behavior of f is defined.^ The., functional criteria of [1.1] are then required to apply only when the arguments of -£ are drawn from Us domain of specification, S . u- ^ - 3) We can postulate new elements of Afunctional domain F corresponding to the values returned by otherwise nonfunctional procedures. We reject the first choice on the grounds that it restricts our consideration to those functions expressible in the lambda calculus, giving us no way of distinguishing between N.and, the ,i«|ui r tivtlys«pwio^B,.Tfte Second choice is rejected after brief consideration, (ip.afgilpwing, wefeioi*) ptrW&ecause of the technical, complications it entails ^ but mtimmrtly because it denies the semantic validity of the interesting <&W^iml*tX*la*%ymLpr* B sl6ria. The third choice seems the most, promising, ftq* t*» pofin* of vt«* ^>f rigorous analysis, but requires a_ substant^ tnt«4^v* imtp- aAotm^atrulxiiag must be carefully scrutinized, This project i* a#proaflfe*<fcfiii subsequent sections? 3.5: Multi-valued Semantic Elements The domain D N of language N was shown, in Chapter .& fco ha** thw^rofiefty that every element x. of D^ corresponds to. ex*^y ; 4ms*U*#i& of a ftinetloiwl : domain; thus each expression x_ in D N has, intuitively, exactly of* semantic value or meaning. In this chapter it was shown that this graceful property of D N is ineogsistea* with the^expressiblity of the function ttHICHFF, a demonstrably computable anduintuitively weii behaved function "'over a particular subset of D^. our i«plea*htati& otWHlC^Ff' while functional oyer this restricted domain S, teehaves^p^oi^y %ften given argUme^ts from D,, which are not in S; furthemore, this annCying tfefVct 14 characteristic of every ' implementation of WHICHFF in a language Wflciehtty powerful as to be " ^ arithmetically complete. The problem^ is, e^dfi* **i HHICHFFois applied to the function FF^: either of the values 2 or ; y is coaaistentwlth^he 1 corres It must be recalled that w* hav* postulated a semantic element • -56- 3.5 definition of WHICHFF [3.3], and there is no implementation of WHICHFF which consistently returns a single value, eg 2, when applied to every x in D semantically equivalent to FF 12 . Thus the evaluation of (WHICHFF FF ) leads to, exactly the same underdetermlned result as the evaluation of (EITHER 1 2): the E values of each expression might be 1 or 2, depending on circumstances which are irrelevent to the semantics of each expression,, 3.5.1: Domains of Specification One means of avoiding such apparently hondeterministic computations is to exclude them from our semantic model, ie, to deny that (EITHER 1 2) has any semantic value. Under this reafrridt ion, we must careMly exclude from our consideration any repression having multiple E values, either by avoiding the use of EITHER and reverting fro the well behaved domain D N> or by assuring ourselves, at each application of EITHER, tfef the result is single valued. We may note, pursuant to the latter program/that for all expressions a. and b_, E[ (EITHER §,&)] is single valued if 1) a. is single valued and b, is meaningless; or 2) b_ is single valued and a. is meaningless; or 3) a, and b_ are both meaningless; or 4) §. and tare each single valued and their values are semantically equivalent. So long as the arguments to EITHER satisfy the above criteria, EITHER is intuitively functional. For each function £ whose: definition invb Ives EITHER, we may then carefully define a domain of specification S f 'such that for arguments * from S f , E[(f x)] i3 sln&Xp ^^ «, ^ for example, show that our definition of WHICHFF in terms pf EITHER is functional over a domain of specification including the functions {FF }. This means of avoiding the semantic difficulties of EITHER may raise certain aesthetic objections. First, it places on us the considerable burden of having to construct domains of specification for each of a large class of functions, and the necessity of showing that each s«ch function is well behaved over its particular domain of specification. SecoftdAt rules out 3-5.1 -57- consideration of algorithms for well behaved functions which have multiply-valued subexpressions. Consider, for an example of the latter limitation, the function f defined so that f[n] = 5, n=1 5, n=2 else undefined. Now, since f[1]=5 and f[2]=5, it is intuitively reasonable to claim that f[either[1 ;2]]=5; yet we cannot make such a claim unless we are willing to assign some semantic value to either[1;2]. 3.5.2: EITHER and the Lambda Calculus There is an essential incongruence between EITHER and the axiomatic basis of the Lambda Calculus which precludes the incorporation of the former as a primitive with an associated delta rule. 1 Recalling that these axioms define an equivalence relation, =, on the domain of the language, incorporation of EITHER results in the equivalences: (EITHER 1 2)=1 (EITHER 1 2)=2 and hence 1=2 from which it follows, by the famous logic of Russel, that "I am the Pope". Clearly the relation between (EITHER 1 2) and 1 is not equivalence, but rather some irreversible reducibility property. Any evaluator which can yield 1 as the value of (EITHER 1 2) cannot be claimed to preserve semantic equivalence; it merely reduces that expression to one of its several values and discards, in the process, information about the other values. This is the underlying reason why N (and the Lambda Calculus) are incapable of expressing WHICHFF, and is basic to the proof of Theorem 3.4. Such a delta axiom is formally ruled out by the requirement that the arguments to primitives be in reduced form, thus restricting applications of fc,±iHh,K to cases where both arguments have meaningful E values. -58- 3.6 3.6: The Power Set Domain * The natural extension of a functional domain F of single-valued elements to a domain F* of multiply-valued elements involves the interpretation of F* as the Power set , or set of subsets, of F. Thus the elements 2 and 3 of F correspond to the unit subsets {2} and {3), respectively, in F*, while the semantic element of F* corresponding to the value of (EITHER 2 3) is the subset {2,3} of F containing both 2 and 3. The meaningless element * corresponds to the empty subset of F, having no value. Other useful relationships which we would like to see in F* include the following; 1)- If s~b in F then {a_,bj~a~b in F». 2) (EITHER (£&)(£ bj)~(£ (EITHER a_ b_) ), or equivalently, the elements {f[a],f[b]} and f[{a,b}] in F» are the 3)The natural interpretation of either on functions leads to the semantic equivalence (EITHER f g)~(LANBDA(X) (EITHER (fX)(g X))). This allows us to propose, in symmetry with (2), that: H) ((EITHER £&) a.) " (EITHER (£ a_) Cga.)). 5) (EITHER a. *)"&. where * is the element corresponding to the undefined computation. 6) If a. corresponds to {a , ...,a.} in F* and b_ corresponds to {b 1t ... ,b.} , then (EITHER a. b.) corresponds to {a..,...,a , b 1t ...,b.} in F*. In general, EITHER of multivalued elements corresponds to the union of the respective elements of F*. 3.7: Interpretation of F* The semantic model being developed in this chapter demands a certain amount of intuitive realignment on the part of the reader. The attractive feature of F* as a semantic domain is that it allows the preservation of a notion of semantic equivalence, without cost in terms of expressibility of certain functions. Its major disadvantage, at least from an intuitive standpoint, is that it requires that we postulate certain abstract semantic elements which 3.7 -59- are intangible in practice — if the expression x_ has multiple values, say 2 and 3, then we have no way of discerning from the value "3" typed by our E interpreter that "2" is also a value of x. We could, of course, build an interpreter which would enumerate the values of x by dovetailing computations at each EITHER juncture. However, as x might have infinitely many values, this process may never terminate; worse yet, even for an x with finitely many values we cannot tell, in general, when all of the values have been typed. There are, however, situations where this ambiguity is unimportant. We may know, for example, that x is single valued, in spite of the dual values of a subexpression y_ of x_. Alternatively, we may recognise that x_ has many values, but be willing to settle for any one of them. 3.8: Computable elements of F* If we have a procedure for identifying the computable elements of a single valued domain F, we can characterize the computable elements of the power set . domain F« as those elements of F» whieh are effectively enumerable sets of computable elements of F. Given an expression X we can enumerate the components of the F» element representing X; one means of doing so is provided in Chapter 6. Furthermore, given an expression G for a function which enumerates a set S of elements of F, we can construct an expression whose representative F* element is S; take for example the expression ((Y (LAMBDA(H)(LAMBDA(X) (EITHER (G X) (H (PLUS 1 X)))))) 0) where Y is the fixed point operator (LAMBDA (Jf> ( (LAMBDA(G ) (F (G G) )) (LAMBDA (G) (F (G G))))). This expression reduces to an expression of the form (EITHER (G 0) (EITHER (G 1) (EITHER (G 2) (EITHER (G 3) )))) and its corresponding element of F» is exactly the range of G. -60- 3.8 We may use as our function G in the above expression an enumerator ENU of the entire domain F, constructed by the techniques of section 3.2.1.2; this expression, TOP, corresponds to the semantic element of F* which is the set F itself. 3.9: Summary This chapter raises the question of the expressibillty of a particular function, WHICHFF. This function is inexpressible £n the lambda calculus, and intuitively it requires a mechanism for multiprocessing for its implementation in spite of its applicative — hence time independent — nature. Two alternative extensions of the N interpreter are proposed, each of which renders WHICHFF expressible: 1) Primitives can be added to N which allow coding and decoding of arbitrary expressions into and from numbers. This mechanism allows programs to access the representation of functions, and it is argued that such a CODE/DECODE facility extends any arithmetically complete language to functional completeness. Yet the use of this mechanism is awkward: the specific implementation of WHICHFF, for example, requires coding an interpreter which simulates the necessary multiprocessing. Moreover the semantic ramifications of CODE are drastic, involving abandonment of much of the applicative structure of any language in which it is embedded. 2) A primitive, EITHER, can be added to N to implement multiprocessing. EITHER renders WHICHFF easily expressible, and it may be Justified semantic ally in an applicative language. In connection with (1), it is noted that although the new primitive CODE is radically nonfunctional, the inverse operation of DECODE (which maps codings into the functions which they represent) is acceptable as an element of our functional domain. A combinatory proof shows that such decoding functions are, in fact, expressible in the unmodified N language; hence we can write in the lambda calculi functions which enumerate the entire semantic domain of these calculi. 3.9 _ 61 _ The introduction of EITHER or equivalent mechanism requires that we modify the structure of the semantic domain and its relation to expressions of a language. In particular, it seems most natural to associate with each expression a s^ of abstract values, rather than a unique single value. We thus move from the domain F of single values to the domain ?• whose elements are enumerable subsets of the elements of F; we term F* the power set domain. The presentation of EITHER in this chapter is informal and relies heavily on implementational notions such as multiprocessing. The following chapters formalize the mechanism in terms of systems of conversion rules, based on the lambda calculus; this process both Justifies and refines the rough implementation model sketched here. This empty page was substituted for a blank page in the original document. * -63- Chapter 4: Theories of EITHER-conversion While the implementation and semantic considerations of the previous chapter provide a strong intuitive basis for the interpretation of EITHER, the further development of this new mechanism requires something more concrete. Specifically, the incorporation of EITHER into a language E involves syntactic manipulations of expressions in E, and hence necessitates a formalism which distinguishes those syntactic manipulations which are semantically valid from those which are not. The relationships developed in the last chapter are analogous to the convention that "(PLUS 2 3)" represents the sum of 2 and 3, without a corresponding mechanism for associating this expression with the expression "5". This chapter begins the project of developing formalisms, i.e. conversion axioms, for the syntactic manipulation of expressions involving EITHER. Several theories (i.e., systems of axioms) are presented in this and subsequent chapters; each is based on the beta-delta 1 calculus, with additional axioms for manipulation of the new EITHER construct. The distinction between these theories stems from an issue of evaluation order, discussed in a following section, and reflects alternative interpretations of certain expressions involving EITHER. A principal difference between the axiom systems presented here and those of the lambda calculus is the introduction of a new asymmetry, in the form of an ordering relation >, between expressions of E. We have seen in previous sections that it is futile to require that E interpretation preserve an equivalence relation; such a requirement was shown to lead to an inconsistency in any language capable of expressing WHICHFF, since (WHICHFF FF 12 )~1 and (WHICHFF FF^)"2 together imply that 1~2. The asymmetry of >, however, allows the relations (WHICHFF FF^)^ and (WH ICHFF FF 12 )>2 to hold without compromising the semantic relation between 1 and 2. We view the relation > as designating EITHER-reducibility, and may interpret x>y informally to mean that the values of y are among the possible values of x. 1 No attempt is made to incorporate eta conversion i »u duucmpu j.s maae to incorporate eta conversion into the svstems nppqpntpH here, although we expect that no new difficulties would arisfin doing so? -64- t We shall use x»y to mean that both x>y and y>x. It is important to distinguish between the relation » and the "reducible to" relation, ->, of the lambda calculus. If the expression X is reducible to the expression Y by means of conventional lambda calculus axioms, then it will follow that X>Y and Y>X; the reverse, however, is not true. The semantic interpretation of X>Y is that every value of Y is also a value of X; i.e., the element of F* corresponding to Y is a subset of the element corresponding to X. 4.1: Preliminary Definitions The terminology of this section is adapted from standard usage in the lambda calculus, and appears e.g in Curry[12], The relation > defined in each of the axiom systems presented here is a monotone relation, i.e. it has the following properties: Reflexivity: For every X, X>X. Transitivity: If X>Y and Y>Z, then X*Z. Monotonicity: If X>Y and B is the result of substituting X for an occurrence of Y in expression A, then B»A. X for an occurrence of Y, then B>A. The above properties are assumed to be axioms of each system. Certain of the axioms to be presented lead to a distinction between the operations of contraction and abstraction : for example, the derivation of S[A;x;M] 1 from ( (LAMBDA(x)M)A), justified by the beta axiom of the lambda calculus, may be termed a beta-contraction. The inverse operation of converting S[A;x;M] to ( (LAMBDA(x)M)A) may be termed a beta-»abstractlon . An expression which is a candidate for contraction is called a redex : thus ( (LAMBDA(x)M)A) is a beta-redex in the lambda calculus. The result of performing a contraction on a redex X is termed the contracture of X. An expression in a particular calculus is in normal form if it contains no Recall that S is the substitution operation of the lambda calculus, Defn [2.6]. 4.1 -65- redex applicable to that calculus. We say further that the expression X is in beta-normal form if X contains no beta-redex, and similarly for the delta, *, and E redexes to be defined presently. The statement that X is in normal form, without further qualification, may be taken to mean that X contains no beta-, delta-, *-, , or E-redexes. We shall often use the notation X{Y} to designate an expression X containing a particular instance of a subexpression Y; having identified an expression with the notation X{Y}, we shall then use an expression of the form X{Z} to denote the result of replacing Y in X{Y} by the expression Z. In this notation, the monotonicity of > is the implication of X{Y}>X{Z} by Y»Z. A relationship of the form A>B is in general derived through a series of steps A 1 >A 2 , A 2 >A_, where each A.>A. .. involves the substitution of an expression Y' in A. for an occurrence of an expression Y>Y'. The monotonicity of > justifies each such substitution, and the transitivity assures that the validity of the entire series follows from the validity of the individual steps. We shall use the terminology Defn 4.1: A reduction step in A from X to Y, for expressions X and Y and a particular axiom system A, is a proof that X>Y by a single application of an axiom of A. Defn 4.2: A reduction sequence from X to X in system A is a series X »X.>...>X such that each X.>X. , is a reduction step in A. 1 n i i+1 4.2: The Either-R Theories The first axiom, common to each of the systems presented, is taken directly from the lambda calculus: Axiom alpha : (Renaming) Let E be an expression of the form (LAMBDA(X)A) where X is any variable and A is an expression, and let Y be any variable not occurring free in A. Then E«(LAMBDA(Y)S[Y;X;A]) . -66- n.? We say that expressions A and B are congruent if A can be converted to B by alpha conversion alone. Congruence is thus reflexive, symmetric and transitive, and to simplify subsequent proofs we shall often allow ourselves to treat congruent expressions as identical* The next axiom is a restricted form of the beta axiom of the lambda calculus, allowing beta conversion only on a beta-redex whose argument is in normal form-: Axiom beta-R : (lambda conversion) Let E be an expression of the form ( (LAMBDA(a_)bJc_) where e_ is &> normal form. Then E*E', where E' is the contract um SLcjssfcJ of E, The following axiom provides a paradigm for delta-conversion, the application of primitive functions to arguments in normal ffcrm. A particular calculus will have a family of delta rules, specifying the behavior of each primitive — e.g. the delta rule lor the primitive PLUS asserting the equivalence of (PLUS n ra) to n+m for all integers n and m. Of interest here is the general form of such rules: Axiom delta : Let E be an expression of the form (ill where A is a primitive function symbol and B is a normal form expression containing no free variables. Then E«E', where E' is the contractual of E derived from B by the (here unspecified) rules associated with A. We may term such an expression E a delta-redex . and the conversion of E to E' is a delta-contraction. Since the relation between E and E' is equivalence, the axiom provides also for the delta-abstraction of E' to E. We note that axioms alpha, beta-R, and delta define a lambda calculus under the equivalence relation w, no use has been made of the asymmetric relation We shall term an expression of the form (EITHER a 1 a-)- f where a, and a ? are arbitrary expressions, an E-redex . We treat the E-r«dex as a new syntactic construct, rather than attempting to classify EITHER as an added primitive function whose operation is specified by delta rules. In particular, we regard the restriction that arguments of primitive functions be in normal form 4 - 2 -67- as unacceptable to the process of EITHER-conversion. Axiom epsilon : (EITHER-contraction) : If E is an expression of the form (EITHER a 1 a 2 ) where a 1 and a ? are expressions, then E>a.. and E>a 2 . Axiom mu: For every expression E, E-( EITHER E E). Axiom rho: (EITHER-distribution) If E is an expression of the form (f (EITHER a b)), where f, a, and b are arbitary expressions, then E-E' where E' is the expression (EITHER (f a)(f b)). The conversion of the redex (EITHER a., a,,) to one of the expressions a or a will be termed an E-contraction. The conversion of an expression E to (EITHER E E) will be called an E -abstraction . 4.2.1: Properties of Either Theories The elementary relationships established in this section hold for subequent theories as well as for Either-R. In addition to their usefulness in proofs, they provide a preliminary reassurance that the Either-R axioms are consistent with the intuitive semantics of EITHER. Thm 4.3: X^Y if and only if, for all Z, Y>Z => X>Z Proof- only if: by the transitivity of >. if: Let Z be Y; then Y>Y by the reflexivity of >, hence X>Y by above hypothesis. The above theorem is consistent with the intuitive notion that X»Y means values derivable from Y are also derivable from X. Axiom mu justifies the trivial abstraction of an expression E to the expression (EITHER E E) ; The following theorem shows that nontrivial EITHER expressions may be abstracted: -68- 4.2.1 Thm 4.4: Let X, A, and B be expressions such that X>A and X>B. Then X»( EITHER A B). proof; By Axiom mu, X»( EITHER X X). But since X*A and X»B, (EITHER X X)>(EITHER A B) by the monotonicity of ». Hence X»( EITHER A B). We may apply this theorem, for example, to the expression A given by A=.( (LAMBDA (X) (PLUS X3))(PLUS 1 2)) By performing single beta and delta contractions, repectively, on A we deduce the relations AXPLUS (PLUS 1 2) 3) A>( (LAMBDA (X) (PLUS X 3)) 3) Application of Thm 4.4 yields the result AXEITHER (PLUS (PLUS 1 2) 3) ( (LAMBDA (X(PLUS X 3)) 3)) This demonstrates that the Either-R theory allows EITHER-free expressions (such as A above) to be converted to expressions containing EITHER. Thm 4.5: X«Y if and only if for all Z, X>Z<=>Y>Z. proof : is by two applications of 4.3. Thm 4.6: For all f, g, and a, ((EITHER f g) a)>(EITHER (f a)(g a)) Proof- By Axiom epsilon, ((EITHER f g) a)Mf a) and ((EITHER f g) a)>(g a); hence, by Thm 4.4, ((EITHER f g) a )>( EITHER (f a)(g a)). The intuitive arguments of the last chapter suggest that the above result could be strengthened to full equivalence (i.e., -) , and this more powerful result may in fact be a theorem in our Either theories; however we have not pursued this equivalence since it is irrelevent to the subsequent proofs. 4.2.2 _69- 4.2.2: EITHER and Evaluation Order Chapter 2 notes the distinction between normal and applicative order evaluation, characteristic respectively of the N and T interpreters. Applicative order evaluation, in which arguments to a function are evaluated prior to the application of the function, is shown in that chapter to lead to the inexpressiblity of certain functions which ignore their arguments. For example, the applicative order evaluation of the expression ((LAMBDA(X)3) A) does not terminate if the value of A is undefined, whereas the normal order evaluation of that expression yields the value 3. The restricted conversion of the beta-R axiom is similar to applicative order evaluation — in each case, the argument to a function must be avaluated (reduced to normal form) before the application of the function (beta conversion). The only distinction between beta-R conversion and the applicative order of the T interpreter is the degree of evaluation required; while Either-R requires that arguments be reduced to normal form, T requires only that they be reduced to lambda expressions or atoms. We may thus, view the restriction on beta conversion as a more serious constraint than the applicative order evaluation of T. The motivation for this restriction in the Either-R system is our intuitively based demand that the axiom of EITHER-distribution, rho, hold. This axiom is in fact inconsistent with the unrestricted beta conversion of the lambda calculus; consider, for example, the expressions I, Z, and F defined by I =. (LAMBDA(X)X) Z = ( LAMBDA (Y) (LAMBDA (X)X)) F _= (LAMBDA (H) (H H) ) Using the axioms of Either-R (notably EITHER distribution) in conjunction with unrestricted beta conversion, we may deduce that I=Z as follows: By Axiom mu, I =. (EITHER I I) and by (restricted) beta abstraction on each of the terms of the E-redex, T = (EITHER (F I ) (F Z)) -70- 4.2.2 since both (F I)=I and (F Z)=I. Then the axiom of EITHER distribution yields I =. (F (EITHER I Z)) from which, using unrestricted beta conversion (as the argument is an E-redex and hence not in normal form) we deduce that I =. (((EITHER I ZXEITHER I Z)) whence by EITHER contraction I > (I Z) = Z Thus we have derived I>Z; to show Z>I (and hence I.Z) we make the deductions I>Z (I Z) MZZ) Z > I using the raonotonieity of > and beta-R abstraction. It follows that, using unrestricted beta conversion in conjunction with the Either-R axioms* we can prove every pair of expressions equivalent — i.e. , the system is inconsistent. We avoid this pitfall it* Eifcher-R by means of the restriction on beta conversion. The beta-R restriction is not, however, the only solution to this problem, and in Chapter 7 an alternative axiom system — designated the Either-K theory — is presented. It should be noted at this point that the restriction on beta conversion is expensive in terms of expressive power. It prohibits, for example, the reduction of the expression ((LAMBDA(X)3) ( (LAMB0A(Y)(I Y) KLAMBDA(Y) (I Y))) to the value 3, since the argument in that expression has no normal form. A more serious drawback is that it interferes with the expressibility of recursive functions since recursion requires, in the lambda calculus, the application of functions to arguments having no normal forms. Chapter 5 is devoted to the mechanism of *-conversion, which mitigate these limitations imposed by the restricted beta conversion. 4.2.3 -71- 4.2.3: Consistency of Either-R An extension of the axiomatic basis of the Lambda calculus may lead to inconsistencies, e.g. the equivalence of 1 and 2. Such equivalences do not hold in the conventional lambda calculus; in particular, the first Theorem of Church and Rosser establishes the consistency of the Lambda Calculus axioms by showing that the proposition X=Y is not provable for any pair of expressions X and Y having incongruent normal forms. We are thereby assured that the equivalence relation = established by the lambda calculus does not place every expression in a single equivalence class, and thus that the cardinality of the domain of the Lambda Calculus is greater than 1. The existence of infinite sets of mutually incongruent normal forms 1 shows that the domain of the lambda calculus is infinite. Moreover, an important theorem of Boehm[20] shows that any axiomatic assertion of the form X=Y, where X and Y are incongruent normal forms, leads to an inconsistency. The theorems of Church-Rosser and Boenm are, not surprisingly, inapplicable to the axiomatic extension presented here. Furthermore, they probably cannot be augmented in minor ways to argue the consistency of the present system, as the uniqueness of normal forms, on which they depend, has been compromised by our extension. Accordingly, is the purpose of this section to establish that the domain of the lambda calculus is a subset of the domain of the Either-R system, and that the new equivalence relation • is consistent with the relation = of the lambda calculus. In particular we wish to show that, for any two either-free expressions X and Y, X=Y if X-Y. Proof of this assertion establishes that 1) The domain of the Either-R system includes the domain of the lambda calculus, hence the new system is nontrivial (having infinite cardinality); and 2) The semantic equivalence defined by the Either-R calculus, applied to EITHER-free expressions, is a subset of the equivalence of the lambda calculus. ete° r exaraple « the set 1= (lambda (x)x), I '=.( lambda (x)I ) , I"=.(lambda(x)I ' ), -72- 4.2.3 It has been noted that in the Either-R system there are expressions X and Y such that X=Y but for which X-Y is not provable ~ a consequence of the restriction on beta conversion which is explored further in the analysis of the R-» system in the following chapter. We precede to the consistency proof, beginning with with the following definition: Defn 4.7: The EITHER-free expression X' is an e^gaidlia of the expression X if and only if X' nay be derived from X by replacing every e-redex (EITHER Xj x 2 ) in X by one of the operands x, or x , Thus the expression X' is an e-residue of X if X' is EITHER-free and X>X' may be demonstrated solely by means of EITHER-contraction (axiom epsilon). Defn 4.8: The expression X is uMtao. if and only if there exists some EITHER-free expression Y such that, for every e-residue X' of X, X'=Y (in the lambda calculus). Thus (EITHER (LAMBDA(X)X) (LAMBDA(Y)Y) ) is unitary, since its e-residues (LAMBDA(X)X) and (LAMBDA(Y)Y) are congruent. We note that EITHER-free expressions are unitary, although unitary expressions are not necessarily EITHER-free, as the above example demonstrates. Furthermore, a unitary expression X may contain subexpressions which are not unitary; witness the expression ( (LAMBDA (X) (DIFFERENCE X X))(EITHER 2 3)) [4.9] whose e-residues are ( (LAMBDA (X) (DIFFERENCE X X)) 2) and ( (LAMBDA (X) (DIFFERENCE X X)) 3) each of which is convertible to by the rules of the Either-R system. Hence expression [4.9] is unitary; it contains, however, the subexpression (EITHER 2 3) 4.2.3 -73- which has e-residues 2 and 3, which are not equivalent under =. Hence the subexpression is not unitary. The proof of the consistency of Either-R is based on the observation that, while EITHER may be introduced into EITHER-free expressions by EITHER-abstraction, the result is necessarily unitary. Moreover, the axioms of Either-R preserve the unitary nature of expressions; we will thus argue that the result of an Either-R reduction sequence on an EITHER-free expression must be unitary. We now introduce a relation which orders expressions by the interconvertability , in the lambda calculus, of their e-residues: Defn 4.10: For any expressions X and Y we say that X encloses Y if, for every e-residue Y' of Y, there is an e-residue X' of X such that X'=Y' in the lambda calculus. Observe that enclosure is reflexive and transitive; the following lemma establishes that it is monotonic: Lemma 4,11: Let Y be a subexpression of X{Y} and let Y enclose Z. Then X{Y} encloses X{Z}. proof : Each e-residue of X{Z} is of the form X'{Z'} where Z' is an e-residue of Z; and for each e-residue Y' of Y there is a corresponding e-residue X'{Y'} of X{Y}. Hence for each e-residue X'{Z'} of X{Z} there is an e-residue X'{Y'} of X{Y} such that Y'=Z"; it follows that X'{Y'}=X'{Z'} hence X{Y} encloses X{Z}. Corollary 4.12: If X{Y} is unitary and Y encloses Z, then X{Z} is unitary and every e-residue of X{Z} is convertible to an e-residue of X{Y}. Lemma 4.13: Let X>Y be a single reduction step in Either-R. Then X encloses Y. -74- 4.2.3 proof : Let U be the subexpression of X which is replaced by an expression W in the reduction step X»Y. By Lemma 4.11, we need only to show that U encloses W to establish that X encloses Y. We exhaustively examine the possible reduction steps from U to W: Case 1: Alpha conversion on U. Then U and W are congruent, and for each e-residue W' of W there is a congruent e-residue U" of U. Case 2: beta-R conversion on U. Let P be a beta-redex of the form ( (LAMBDA (X)M{X})A) where A is in normal form, and let Q be the eontractum S[A;X;M{X}] of P. Then every e-residue P' of P is of the form ( (LAMBDA (X)M'{X})A) where M'{X) is an e-residue of M{X} , and there is one such e-residue P' for every e-residue M' of M. Each e-residue W of W is of the form M'{A} and there is one such e-residue W for each e-residue M' of M. For each M' the corresponding e-residues of P and Q are ( (LAMBDA (X)M'{X}) A) and M'{A) respectively, which are interconvertible in the lambda calculus by a single beta conversion; hence P encloses Q and Q encloses P. W is either a beta-R contraction or a beta-R abstraction of U, hence U encloses M. Case 3: delta-conversion on U. If either U or W is a delta redex, then both U and W are EITHER-free and thus U encloses W. Case 4: EITHER contraction. If U is an expression of the form (EITHER A^ ^ clearly U encloses both A 1 and A ? ; each e-residue of W is an e-residue of A. or of Ap. Case 5: EITHER-abs tract ion. Then W is of the form (EITHER U U), and each e-residue of W is an e-residue U" of U. Case 6: EITHER-diatribution. Let P be an expression of the form (EITHER (F A)(F B)) and let Q be (F (EITHER A B) ) The e-residues of P consist of all the expressions of the forms (F' A') and (F' B') where F', A', and B' are respectively e-residues of F, A, and B. We note that the e-residues of Q consist of exactly the same set of expressions, hence P encloses Q and Q encloses P. Thus for a conversion 4.2.3 _ 75 _ U>W of the forms ?>Q or Q>P, U encloses W. This completes the proof of Lemma 4.13. We present the obvious generalization of this result as Corollary 4.14: Let X and Y be expressions such that X>Y in the Either-R system. Then X encloses Y. £rpof follows directly from Lemma 4.13 and the transitivity of the enclosure relation. This corollary shows that the ordering > of the Either-R system implies enclosure; thus the number of distinct (under = of the lambda calculus) e-residues of an expression X can only be decreased by a reduction step in Either-R. While each reduction step may introduce new E-redexes (by EITHER-abstraction), the terms of each redex so introduced are necessarily interconvertable. The consistency of the Either-R theories is a special case of this corollary: Thm 4.15: Let X and Y be EITHER-free expressions such that X>Y in the Either-R theories. Then X=Y in the lambda calculus. erpof: By Corollary 4.14, X encloses Y; since X and Y are each EITHER-free, X and Y are respectively e-residues of X and Y. Hence X=Y in the lambda calculus. The above theorem establishes that the Either-R theories are consistent in the sense that they introduce no new equivalences between expressions which are distinct in the lambda calculus; and are hence of infinite cardinality. It is noteworthy at this point that the above proof, specifically Lemma 4.13, depends on our restriction on beta conversion, when unrestricted beta conversion is allowed (as in the Either-K theories presented in Chapter 7) it is not true in general that every beta-redex X encloses its contractum X', as demonstrated by the beta redex .76- 1-2.3 A= ( (LAMBDA (X) (PLUS X X))(EITHER 2 3)) whose e-residues are each convertible to 2 and 3, respectively, while the contractual of A (PLUS (EITHER 2 3) (EITHER 2 3)) has an e-residue (PLUS 2 3) which is convertible neither to 2 nor to 3. 4.3: Summary This chapter defines the ground rules for the axiomatization of Either theories and presents the Either-R theory. fRiile the usefulness of this system is limited due to the restriction placed on beta conversion, it develops much of the mechanism to be used in subsequent chapters. The principal distinction to be made between the Either theories lies in the circumstances in which beta-conversion is allowed. The Either-R Theories, which prohibit beta-conversion unless the argument to be substituted is in normal form, allow the distribution of functions over the terras of an EITHERexpression - a relationship which we find intuitively gratifying. Unfortunately this restricted beta-conversion results in a very weak theory, a problem to which the next chapter is devoted. The Either-R theory presented in this chapter is shown to be consistent in the sense that X»Y, where > is the ordering defined by the new axioms, is not a tautology. The proof is based on the consistency of the lambda calculus; specifically, it is shown that, for expressions X and Y which are EITHER-free (and thus admissible syntactically in the lambda calculus) X>Y implies the interconvertability of X and Y. This general technique will be followed in subsequent consistency proofs as well. 5 _77- Chapter 5: •-Conversion It was noted in the previous chapter that the restricted lambda conversion of the beta-R axiom, i.e. the requirement that the argument of a beta-redex be in normal form before the contraction of that redex, severely limits the expressive power of languages based on the Either-R theory. In particular, the inexpressibility of recursive functions constitutes an intolerable restriction since it renders such languages functionally incomplete. The mechanism of *-conversion, to be introduced in the present chapter, ameliorates this limitation by extending the ordering relation > in a way which is consistent with its function in the Either-R theory. Although •-conversion and EITHER reduction are in an important sense complementary operations, their respective mechanics may be dealt with separately; thus for the purposes of this chapter we temporarily disregard the axioms of EITHER conversion. In Chapter 6 we combine the two mechanisms. The semantic interpretation of > suggested by the Either-R theory is one of inclusion gf values; it was noted that X»Y signifies, in general, that each value of Y is also a value of X. The corresponding relation in the semantic domain F* is set theoretic inclusion. Thus if x and y are the semantic elements of F« corresponding to X and Y, respectively, then X>Y implies that y is a subset of x. Consistent with the semantic notions of Chapter 3, the expression (EITHER X Y) corresponds in F» to the union of the elements x and y. It was further suggested that the undefined computation corresponds, in F«, to the empty set — i.e., it has no values whatsoever. This chapter develops the syntactic analog of the empty set in F*. Specifically, the new syntactic element « is introduced as the canonical normal form representation of the undefined computation. The interpretation of > as set theoretic inclusion in F* suggests that, for every expression X, X»« (since every' set has the empty subset). It would seem, then, that the consummation of the semantics of EITHER reduction requires that its syntactic mechanism reflect this aspect of the structure of F*. -78- 5.1 5.1: The R-* Theories We now focus our attention on "-conversion and its relation to the restricted beta conversion. To this end we consider the R-* system whose axioms include alpha* beta-B, and delta discussed previously, in addition! to the following: Axiom sigma : ( "-contraction) : For every expression E» E»*. Thus * is an expression in the R-» system which Is lower, in the sense of >, than every other expression:, ttiile every/ expression; is reducible to *, * is itself only reducible to * Cas * is not a beta- or delta-redex, and contains no variables). Defn 5.1: An expression of the form C* A), where A is an arbitrary expression, is called a * -redex . Consistent with our previously defined notion of normal forms, we shall henceforth require an expression X to contain no *-redexes if it is in normal form. Hoting that the only conversion which may be performed on a *-redex without resulting in another *-i>eAex is its replacement by *, we shall say that the con trac turn of a *-redex is *. 5.1.1: Significance of normal forms The restricted lambda conversion allowed by the beta-R axiom bears a curious resemblance to the lambda-I calculi of Churchill. In these systems, Church specifically prohibits expressions of the form CLA*®JA(X)M)S unless the variable X appears free ia the body Wj thus the lambda-I systems exclude, in general, functions which ignore their arguments. A principal consequence of this restriction is the fact that, for expression X to have a normal form, every subexpression of X must have a normal form, le note, with passing interest, that the normal fbrm restrictis* of hefta-B allows us to derive any normal fbm in the lambda-I calculus which is possible using unrestricted beta conversion; this follows from the observation that in the lambda-I system we can always reduce the argument in a bsta-reoex to normal form before contracting the redex. 5.1.1 -79- Church's preference for the lambda-I over the unrestricted "lambda-K» 1 theories stems from the elusive nature of those expressions having no normal forms. The theorem of Boehm assures us that expressions having incongruent normal forms are semantical ly distinct, and the theorems of Church-Rosser guarantee that equivalences between expressions having normal forms are decidable. The semantics of normal forms is consequently uncomplicated: every pair of semantically equivalent normal form expressions is provably equivalent, and for every pair of incongruent normal forms we can find a context in which they produce different values. The admission of expressions having no normal forms compromises this situation severely. The requirement that a semantic equivalence relation be exfrensional , i.e. that equivalent expressions produce equivalent values in identical contexts, leads tea distinction between semantic equivalence and the equivalence of interconvertability under the lambda calculus. Scott[22], for example, demonstrates an infinite sequence Y, Y ... of fixed point operators which are not convertible to one another despite the fact that they produce the same values when embedded in identical contexts. The problem of constructing a functional domain for the lambda calculus is fundamentally equivalent to the definition of an extensional relation of semantic equialence over the expressions of that calculus, a project whose recent success is due to Scott. The technique used by Scott[5,6,22] involves the notion of successively better approximations to the abstract semantic element represented by an expression X, so that the semantic element associated with X becomes the limit of this sequence of approximations. In the Scott model, a function f approximates every extension f of f'; more generally, f ' approximates f if and only if for every z, f'[z] approximates f[z]. This notion of approximation seems essential to the interpretation of domain elements as functions, largely because the theories of functions with which we are familiar employ type restrictions ruling out self-application. 2 r.-nSJ^f^Il2i a ? d 'Sir ryC , 12] , ref er to the unrestricted conversions of the 2rtSyt2fh?i n fi tam £da calculus as lambda-K conversion, presumably because of the I is SSiiJS f2L t ?L COHlb i n ? fc ? r . K f- ( 45P^ (X)( fe AMBDA ^> x >) in t^se systems? boSd^S^W& r b^ of the fhi n ;^.^Ti ieu i a rt < LA «fDA(X)(X X)) is difficult to interpret as a function in fSotiSl K^r 1 ^"?' Hindley[21] speculates that a theory of n™Si?2Si-i ) 5 se ?i 0n com 5inatory logic, rather than set theory, might ?2SiS SSiListS self - a PP llcati °"; while awaiting further developments we -80- 5.1.1 The mechanism of "-conversion presented in this chapter is reminiscent of the Scott construction. Specifically, we introduce means by which the various approximations of an abstract semantic element can be represented as expressions in the language itself, and provide for the syntactic conversion of an element X to an approximation X' of X. We have thus come to view "-conversion as a syntactic analog of the Scott construction in which approximations are expressed in the domain of the language rather than in the abstract semantic domain. The addition of *-conversion to the lambda calculus leads to a multiplicity of normal forms for every expression. We shall see, for example, that the Y operator Y=.(LAMBDA(F)((LAMBDA(H)(F(H H)))(LAMBDA(H)(F(H H))))) which has no normal form in the conventional lambda calculus, has infinitely many normal forms (LAMBDA(F)(F *)) (LAMBDA(F)(F (F *))) (LAMBDA(F)(F (F (F »)))) when •-conversion is admitted. Each of these normal forms may be interpreted as an approximation to the Y operator, and in any context where Y gives a normal form value, one of the above normal forms of Y will give an identical value. Since the semantic element associated with each of these normal forms is clear (in the sense that normal forms are semantically distinct) we retain something of the semantic simplicity of the lambda-I calculus. The semantic value of a given expression is simply the set of normal form values of that expression, and expressions X and Y are semantically equivalent if and only if they have identical sets of normal forms. One of the motivations for •-conversion is to enable us to retain the power of the unrestricted (lambda-K) calculus while restricting beta conversion. It is intuitively reasonable to expect that one can always find a sufficiently close approximation to the argument of a lambda expression that the restriction on 5.1.1 -81- beta conversion becomes unimportant where '-conversion is allowed, and much of the remainder of this chapter is devoted to the proof that this is in fact the case. 5.1.2: Theorem on Normal Forms The main result of this section sheds light on the ordering (under » of the normal forms derivable in «-» from an expression It. We begin with the following definition, adapted from Curry[12]: Defn 5.2: Let P be a redex and Q be a subexpression in an expression B, and let B' be the result of replacing P by its contractual P' in B. We define the residues £f_ fl with respect to. P as subexpressions of B' designated as follows: Case 1: P and Q are the same redex in B. Then Q has no residual with respect to P. Case 2: P and Q are non-overlapping subexpressions of B. Then the residual Q' of Q is that subexpression in B' which is homologous 1 to Q in B. Case 3: P is a subexpression of Q. Then the residual of Q in B' is the expression Q' which is homologous to Q in B. We note that the occurrence of P in Q has been replaced by P' to make Q'. Case 4: P is a beta-redex ((LAMBDA(X)M)A), and Q is a subexpression of A. Then P' is S[A;X;M] and contains n instances of A corresponding to the n free occurrences of the variable X in M; let these instances of A be identified as A ( ... A R . Each Ai contains an instance Qi of the redex Q; these n expressions Q^ ... Q Q are the n residuals of Q in B'. Note that n may be zero, in which case we term the contraction of P a cancellation and Q has no residuals. homologous subexpressions occupy the same relative position in their containing expressions; thus A in ((X (HA) Z) Y) is homologous to B in ( (P (Q n r independently of the structure of the subexpressions X, W, Z, Y, P, W i Hj a no o« -82- 5.1.2 Case 5: P is a beta-redex ( (LAMBDA(X)M)A) and Q is a subexpression of M. Then P" is S[AjX;M] and the residual Q' of Q is the subexpression of P* which is homologous to Q in M. Case 6: P is not a beta-redex, and Q is a subexpression of P. Then Q has no residual in B*. Informally, a residual of an expression Q is an image of Q after a contraction. Consider, for example,, the residuals of the subexpression (PLUS 3 *) in the beta-redex (OAMBMCXXFLHS X I))(PLOS 3 *)J [5.31 whose contractus is the expression CPLBB CPLHS 3 *>(PUB 3 *>> We note that the two residuals of the subexpression (PUB 3 4) of expression [5.3} are the occurences of CPLBS 3 *) in the eontractum. Contraction in the delta redex (PUB 3 ' *> in empreasios [5.31 yields the residual CCEJUSMCXKPLIB X X>) ?> We shall occasionally find it useful to speak of the residual of an expression Q after a series of contractions; we amy thus refer to Q as a resldal of Q with respect to the sequence of contractions B£& >...>B if there is a in subexpression C^_ t of B^-t such that Q^ is a residual of Q and C^ is a residual of $». Thus consecutive beta- and delta-contractions on expression [5.3J yield (PLUS 7 (PUS 3*)) which contains a single residual of the subexpression (PLQS J t). The following leans establishes that, the residual of a redex is always a redex: Lemma 5.4: Let P and Q be red exes in an expression B t and let Q* be a residual of Q with respect to P. Then Q' is a redex. proof: we consider the following collectively exhaustive cases: 5.1.2 -83- Case 1: P and Q are non-overlapping. 1 Then Q' is the same redex as Q. Case 2: P is a subexpression of Q; we consider the cases of the syntax of Q: a) Q is a beta-redex of the form ((LAMBDA(X)M A). If P is a subexpression of M, then Q' is the beta-redex ((LAMBDA(X)M')A). If P is a subexpression of A, then Q' is the beta-redex ( (LAMBDA (X)M)A'). b) Q is a »-redex of the form (• M); then P must be a subexpression of M, and Q' is the «-redex (* M'). c) Q cannot be a delta-redex, as it contain P. Case 3: Q is a subexpression of P; we consider cases of the syntax of P: a) P cannot be a delta-redex, as it jontains the redex P. b) P cannot be a »-redex, as then Q would have no residual. c) P is a beta-redex of the form ( (LAMBDA (X)M) A) where Q is a . subexpression of A. If Q is cancelled by the contraction of P, then Q has no residual; hence M must contain 1 or more free occurrences of X. Then each residual of Q is the redex Q itself. d) P is a beta-redex ((LAMBDA(X)M)A) where Q is a subexpression of M. We examine syntactic cases of Q: i) Q is a delta-redex; then Q' is identical to Q, since Q may contain no free variables (in particular, no free occurrence of X). ii) Q is a *-redex (* M). Then Q' is the »-redex (« M'). iii) Q is a beta-redex ( (LAMBDA(Y)B)C). Then Q' is a beta-redex of the form ( (LAMBDA (Y)B' )C'). 1 othe"r. eXPreSSi ° nS are "^-overlapping if neither is a subexpression of the -84- 5.1.2 The converse of the above lemma is not in general true, i.e., the residual P' of P may be a redex even though P is not. Consider for example the expression P a. (((LAMBDA(X)(LAMBDA(Y)Y)) 3) 4) which is not a redex. Contraction of the beta-redex in P yields the residual P' of P given by P' =. ((LAMBDA(Y)Y) 4) which is a beta-redex. We should like to distinguish between reduction steps in R-* which are contractions and those which are abstractions; for this distinction the following notation is convenient: Defn 5.5: A contraction step A»>B is a single reduction step from A to B which is either a beta-, delta-, or '-contraction. Defn 5.6: A contraction sequence A () »A 1 »...»A n from A Q to A n is a reduction sequence from A. to A containing only alpha-conversions and contraction steps. The length n of such a sequence is the number of contraction steps in the sequence. We now examine contraction sequences which terminate in normal forms beginning with Lemma 5.7: Let X{Y} be an expression containing a redex Y, and let X{Y}>>. ..>>X' be a contraction sequence of length n, where X' is in normal form. Then there is a contraction sequence X{Y'}>>. ,.>>X', where Y' is the contractum of Y, of n or fewer steps. proof is by induction on n. basis n=1: X' contains no redex, hence Y must be either contracted or cancelled (by a beta- or *-contraction). If Y is contracted then X[Y']»>X' by the null sequence. If Y is cancelled then X[Y']>>X' by the same contraction as X[Y]»>X'. 5.1.2 -85- induction: We assume the lemma to be true for sequences containing n or fewer steps. Consider the first contraction step X[Y]»X in the n + 1-step sequence X[I]»„.»x' f and let Y r .. Yj be the j 1 residuals of Y in X r If j=o then the argument in the basis applies, as Y is either contracted or cancelled in the first step. If j>0, j applications of the induction hypothesis establish that X, '»...»!' in n -1 or fewer steps, where X 1 ' is the result of contracting each Y i in X,. But X[Y']»X ' in a single step; hence X[Y']»X' in n or fewe/steps. The significance of Lemma 5.7 is that the contraction of a redex Y in expression X cannot pxfllflaa the reduction of X to normal form. Informally, we expect that if the subexpression Y plays a significant role in the evaluation of X, the contraction of Y will shorten the reduction of X; if, however, Y is irrelevent to the value of X then Y may be replaced by an arbitrary expression with no effect on the evaluation of X. This consideration motivates Lemma 5.8: Let B^B^. . ,»B n be a contraction sequence of length n, and let B n be in normal form. Let P be a redex in B Q , and let P' be the contractum of P. Then one of the following applies: a) There is a contraction sequence B*»...»B n of n or fewer steps, where B« is the result of substituting * for P in B ; ojl b) There is a contraction sequence B'»...»B n containing fewer than n contraction steps, where B' is the result of replacing P in B by P'. praoX is by induction on the length n of the contraction sequence B„»B . n bgsis. n=1 ; then B »B n in a single contraction step. Let Q be the redex contracted in B Q »B n . If Q i3 the same redex as P, then B' is identical to B n , and (b) is satisfied. Otherwise P must have no residual in B , since B n i s in normal form and any residual of P is a redex. Then P^ust be cancelled by a beta- or '-contraction in B Q »B n , and (a) is satisfied. induction : n>1. Consider the redex Q contracted in the step B » B . if Q is the same redex as P, then (b) is satisfied as before. Otherwise we consider the J residuals P r .. Pj of P in B,. If j. then P is cancelled -86- 5.1.2 in the step B^B^ and (a) applies. If j>0, we apply (by the inductive hypothesis) the lemma to the contraction sequence B.j». ..»B n , whose length is n-1 : Case 1: Each residue Pi in B 1 is convertible to •; i.e., (a) applies to each Pi. Then (a) applies to P in B Q , as B*»B 1 * in a single step, where B» is the result of replacing each Pi in B 1 by *. Case 2: Some residue Pi of P in B is not convertible to *; i.e., (b) applies to Pi. By Lemma 5.7, contracting any P R in B 1 cannot prolong the sequence B t >>. ,.»B ; by the induction hypothesis, there is at least one P^ whose contraction shortens the sequence. Then if B ' is the result of contracting each P in IL t there is a contraction sequence B„>>. ..>>B in fewer than n*1 steps. Since B'»>B ' in a l n « single contraction step (of the same kind as BQ»B.,)"(b) is satisfied. This completes the proof of Lemma 5.8. The following theorem establishes a fundamental property of »-conversion. Informally it ensures that, for any two normal form expressions A^ and A 2 » which are each derivable from an expression A, there is an expression A* in normal form which is an upper bound of A^ and k£ in the sense that A'^A,' and A*»A *, and furthermore that A»A*. This result is then extended to the case of an arbitrarily large finite set of expressions A 1 *...A n each derivable from A. The existence of normal form upper bounds of arbitrary sets of expressions derivable from A is essentially equivalent to the proposition that A can be approximated, to arbitrary accuracy, by normal forms derivable from A. Thm 5.9: Let A* and k* be normal form expressions and let A be any expression such that A»A • and A»A *. Then there exists an expression A* in normal form such that A»A*, A**^*, and A*»A 2 «. proof : Let P[n;m] be the proposition that Lemma 5.9 is true for every A, A * and A J* such that: (i) A»A • in n., steps and A»A 2 * in n 2 steps, where n^^n; and (ii) A contains m or fewer redexes. * 5.1.2 -87- Then the lemma is true if and only if P[n;m] is true for all n and m; we procede in the following steps: 1) For every n, P[n;0] is true since in these cases A contains no redex and is consequently in normal form. 2) For every m, P[1;m] is true since in these cases either A=A » or A=A •; hence A must be in normal form and A*=A. 3) If for some n and m and for all j P[n,j] and P[n+1;m] are true, then P{n+l;m+l3 is also true. proof : Let A, A*, and A * be expressions such that the premises of P[n+1;m+1] are satisfied; then A contains m+1 or fewer redexes, and n^n^n+l wner€ n i and n o are tne res P* et < ive lengths of the sequences A»>A • and A*>k*. We now choose an innermost redex Y of A, i.e. a redex Y which contains no other rede:. Such a redex Y must exist unless A is in normal form, which is ruled out because m+1>0. Let A{Y} denote A (which contains Y as a subexpression) and let Y' be the contractum of the redex Y. Then by Lemma 5.8, one of the following applies: a) Af*}*^* in n^ or fewer steps, and A{*}»A 2 » in n_ or fewer steps. b) A{Y'}>>A * in n ' steps and A{Y'}>A * in n„' steps, where n 1 *+n 2 '<n 1 +n 2 . If case (a) applies, then A{M has fewer than m+1 redexes, and by P[n+1,m] the proposition P[n+i,m+1] is true. If (b) applies, then P[n+1,m+1] is true if P[n;j] is true (where j is the number of redexes contained in A{Y'}); by hypothesis, P[n;jJ is true for all j, hence P£n+1 ;n+1 ] is true. 4) If for all j P[n;j] and P[n+1 ;03 are true, then for all i P[n+1,i] is true. proof is by induction on i. P[n+1 ;0] follows directly from (1); P[n+1;i+U follows from (3) and P[n+t;i]. -88- 5.1.2 5) For every i and j, P[i;j] is true. proof is by induction on i. basis ; from (2), P[1 f j] is true for all j. induction : Assume that P[i;j] is true for all j. By (1), P[i+1 ;0] is true; hence by (4), P[n+1;jJ is true for all j. This completes the proof of Theorem 5.9. The proof of Theorem 5*9 involves a succession of steps from the expression A to the normal form A*, such that the result A of each step retains the property that A >>A^» and A.»A 2 *. The moderate complexity of the proof stems from the obscure sense in which each step comes "closer" to A*; by Lemma 5.8, each successive step from A to A. - either: i) Reduces (by one) the number of redexes, while keeping the total number of steps in the contraction sequences A.»>A..» and A,»A 2 * constant; oji ii) reduces the total number of contraction steps, while changing (increasing or decreasing) the number of redexes by some arbitrary finite amount. The proof of Theorem 5.9 is essentially a demonstration that A* can always be derived from A by such a sequence in finitely many steps. The generalization to arbitrary finite sets of normal forms follows naturally: Corollary 5.10: Let A be any expression and let A... .A, be expressions in normal form such that, for each i, A>>Ai. Then there exists an expression A 1 in normal form such that A»A* and, for each i, A*>>Ai. proof is by induction on j. basis : For j>2, the corollary is trivially true; for j=2, it is true by direct application of Theorem 5.9. induction : Assume the corollary is true for each set A....Ak containing fewer than J expressions. By Theorem 5.9, there is an expression A 2* in normal form such that k.2*»k^ and A.,2»>>A 2 and A>>A T 2*; by the induction hypothesis, we can now find an upper bound of the set A 2*, A3,..., A 5.1.2 -89- which contains j-1 expressions; let A* be the normal form upper bound of this latter set. But, since k*»k^2*, it follows that A*»>A 1 and A>>A 2 ; hence for each Ai, A*>>Ai, and A* is the required upper bound. The final theorem of this section establishes that, for the evaluation of any particular expression X{Y} (i.e., the reduction of that expression to a normal form) there exists a sufficiently good approximation Y* of Y such that Y* is in normal form: Thm 5,11: Let X{Y}>>. . .>>X* be a contraction sequence of length n, where X* is in normal form. Then there exists an expression Y* in normal form, such that Y»Y« and X{Y«}»X». proof is by induction on the length n of the contraction sequence. If n=0, then Y is in normal form and is the required Y». If n>0, we consider the residuals Y.....Y. of Y in X.. By the induction hypothesis each Y. can be contracted to a normal form Y » and the result X * of replacing each Y. in X 1 by If is such that X^^X*. Since for each i Y»Y i «, by Corollary 5.10 there is a Y« such that Y»Y« and for each i Y*»Y . Then X{Y}»X{Y«}»X 1 ». ..»X». We may speculate further on the structure of the set S of normal forms of an expression A. The above theorem shows that any finite subset of S has an upper bound in S; since * is in S, we may claim further that each finite subset in S has a lower bound in S. It seems likely that S forms a lattice ordered by >, which is to say that each finite subset of S has both a least upper bound and a greatest lower bound. In general such a lattice of normal forms can be complete only for those expressions which have normal forms in the lambda calculus. 5.1.3: Relation to the Lambda Calculus In this section we demonstrate a sense in which the R-* theory is as powerful as the (unrestricted) lambda calculus; , in particular, we show that any expression A which has the normal form A' in the lambda calculus has the same -90- 5.1.3 normal form in R-*. Thm 5.12: Let A-->A„->. . .->A be a sequence of beta- and delta-contractions 1 n in the Lambda calculus (possibly intermixed with alpha conversions), and let A^ be in normal form. Then A A »A in R-*. n On proof is by induction on n, the number of contractions in the sequence A n ->...->A . n basis n=0; then A and A are identical, and the theorem is trivially true. induction ; n>0; we assume then that A.>>A and must show that A >>A Q . We procede by showing that A »A,. for each of the possible contraction steps A ->A... If the contraction step is an alpha- or delta- conversion, then the same contraction can be performed in R-* hence A.»A 1 ; we thus need only consider the case where A ->A 1 by a beta contraction. Let P be the beta-redex contracted in the step A ->A..; then P is of the form ((LAMBDA(X)M{X}) Y) and the contracture P' of P is of the form M{Y}, containing j instances (residuals) Y.....Y of the argument Y. By Theorem 5.1 1 each Y t may be contracted in R-* to a normal form Y^, such that A.,»>>A n where A^ is the result of replacing each Y ± by Yj*. By Corollary 5.10 there exists an upper bound Y* such that Y»Y» and, for each i, Y**^. By contraction of the subexpression Y of A Q {Y} we have A {Y}»A {Y«}; since Y* is in normal form, the beta contraction of the redex P* in A Q {Y»} ((LAMBDA(X)M{X)) Y» ) yields a contracture M{Y*} containing j instances of Y». But each instance of Y* may be contracted to the corresponding Y^, hence A () {Y»}»A 1 «. Then we have A () {Y}»A {Y*}»A 1 »»A nI and A Q »A n in R-*. The simplest illustration of the use of "-conversion to mitigate the beta-R restriction involves the evaluation of the expression A given by A = ((LAMBDA(X)3) B) 5.1.3 -Q1- where B = ((LAMBDA(H)(H H) )(LAMBDA<H) (H H)) ■ince B has no normal form in the conventional lambda calculus (or, as a consequence, in Either-R) the beta-redex A cannot be contracted under beta-R. Hence A has no normal form in Either-R; in R-*, however, •-contraction on the subexpression B of A yields A > (<LAMBDA<X) 3) •) which may be contracted, under beta-R, to the value 3. We thus can derive the value 3 from the expression A, despite the restriction on beta conversion. We may of course derive other normal form values of A which involve the element *; these may be interpreted as "approximations" of the value of A in the sense that they retain partial information concerning the value of A. In this light the expression • itseOLf is a particularly bad approximation of A, as it gives no clue about the value of A. The expression 3 (which is, significantly, *-free) i.s a perfect approximation of A since it contains all of the information necessary to .-.derive the value of A — i.e,, A=3 in the lambda calculus. 5.1.4: Consistency of R-* Theories We observe, at this point, that the addition of the *-conversion axiom to the lambda calculus does not lead to inconsistency; specifically, if X and Y are •free and X>Y in an R-* Theory, then X=Y in the corresponding Lambda calculus. The intuitive justification for this claim stems from the unidirectional nature of "-contraction - there is no corresponding abstraction operation. Thus if the reduction X»Y involves the *-contraction of a subexpression U, then U must be cancelled since Y is *-free. The consistency of the R-* Theories follows as' a special case of the consistency of the Either-R-* Theories, which is proved in the next chapter; consequently no proof is given here. 5.2: Applications to the Lambda Calculus -92- 5.2 The theorems of this chapter may provide tools of general usefulness in the study of the conventional lambda calculus. Suppose, for example, that neither of the expressions X and Y have normal forms in the beta-delta calculus, and that furthermore they are not interconvertible. He may still suspect, however, that they are equivalent in an extensional sense. In particular we may wish to prove that if either of Z{X} or Z{Y} has a normal form in the lambda calculus then Z{X}=Z{Y}. The mechanism of "-conversion suggests a technique for constructing such proofs. Suppose we could show that in R-* the expressions X and Y have identical sets of normal forms. 1 From Theorem 5. t1 it then follows that, for a^iy Z and every Z* in normal form, Z{X}»Z* if and only if Z{Y}»Z«. But Theorem 5.12 extends this extensional equivalence to th£ lambda calculus; hence for any Z and any normal form Z», Z{X}->Z» if and only if Z{Y}->Z* where -> denotes lambda calculus reduction. We deduce from these observations that any two expressions which have interconvertible sets of normal forms are eqivalent in this important extensional sense. We may apply, for sake of illustration, the above technique to the example cited by Scott 2 of the two fixed point operators Y^CLAMBDACFXZ Z) ) and Y t =(Y (LAMBDA(Y)(LAMBDA(G)(G (Y G))))) where Z is the expression (LAMBDA(H)(F (H H))) Y and Y 1 are not interconvertible in the lambda calculus, and neither has a normal form. Noting that Y contains the single redex (Z Z), the unique single contraction which can be made reduces Y Q to the expression (LAMBDA(F)(F (Z Z))) 1 Specifically, we must show only that X»X» implies Y>Y»»X« and conversely, where X* and i* are any normal form expressions. 2 Scott[22] credits the example to Corrado Boehm, and acknowledges an unpublished proof due to David Park that the expressions Y n and Y 1 are equivalent in the Scott formalism. u 5.2 -93- which again contains the single redex (Z Z). It becomes clear from the sequence of reductions that this process leads to the conclusion that the normal forms (in R-») of Y are all of the form (LAMBDA(F)(F (F (F (F ... (F ») ... ))))) and for every natural number n there is a normal form Y » n whose body is F applied to • n times. We now refer to the definition of I... By Theorem 5.11, for every normal form Y^ of Y^Yq} there is a normal form Y Q » such that Y 1 {Y Q «}»Y 1 '. Hence every normal form of Y. is a normal form of Y^Yq*"} for some for some n. But each of the latter is of the form (G (G (G (G ... (G *) ... )))) where G stands for the expression (LAMBDA(Y) (LAIffiDA(G) (Y G))). But (G «) reduces to (LAMBDA(G)(G <• G))) from which, by contraction Of its »-redex, we arrive at Y •1=.(LAM8DA(G)(G *)). Then Y^sXG I «1) has as its maximal normal form (LAMBDA<G)(G XG •))); and it becomes clear from this informal argument that each R-* normal ibrm Y • n of Y 1 is of the form <LAMBM{G)(G <G <G <G ... (G *) ... ))))) whose body contains n applications of G. Thus each normal form derivable from Y_ in R- 1 is derivable from Y.., and conversely. Now if, for some X, X{Y-}=X* in the lambda calculus where X» is in normal form, then by Theorem 5.12 X{Y Q }>X* in R-». Then by Theorem 5.11 there is a normal form Y » n of Y Q such that X{Y Q « n }>>X»; since Y 1 has a normal form Y 1 * m »Y () » n , then XfY^^X* hence XM^sX* by the consistency of R-*. An entirely symmetric argument shows that X{Y..}=X* implies X{Y„}=X*. 5.3: Summary The mechanism of *-conversion introduced in this chapter allows expressions to be approximated, to arbitrary accuracy, by expressions in normal form. The initial motivation for ^-conversion is the mitigation of the limitations on expressive power imposed by the restricted beta-conversion, but the techniques -94- 5.3 of this chapter may be useful generally in the lambda calculus. The principal technical results of the chapter are: 1) The introduction of • as a canonical representation of the undefined (nonterminating) computation, and the axiom on star conversion asserting that, for every X, X»». This axiom is motivated by the interpretation of > as denoting set theoretic inclusion in F*; the empty set, corresponding to the undefined computation •, is a subset of every element of F». 2) Theorem 5.9 and its corollary establish that for any set A «...A » of 1 * " n normal forms derivable from an expression A. in R-*, there exists an expression A* in normal form such that A»A* and A«>Ai for each i<n. 3) Theorem 5.11 shows that if expression X{Y} is reducible to Z* , a normal form in R-*, then there exists a normal form Y» such that Y»Y* and X{Y«}»Z*. Informally this result assures us that, for every expression Y and every context X{Y}, there is a sufficiently good normal form approximation Y» of Y. The previous result (2)then guarantees that, for any finite set of approximations of Y, we can find a normal form Y* which may be used in lieu of any member of the set. *») Theorem 5.12 provides the final tie to the lambda calculus, by showing that every normal form derivable in the lambda calculus is derivable in R-«. The R-* Theory is thus as powerful, in an important sense, as the lambda calculus with unrestricted beta conversion. Furthermore, the R-* Theories suggest a natural test for extensional equivalence of expressions: the interconvertabillty of normal forms. This technique is applicable to the lambda calculus, and the extensional equivalence of noneonvertible fixed point operators Y Q and Y. is used as an illustration. The development of •-conversion in Chapter 5 is independent of the EITHER reduction of the previous chapter. The combination of the two mechanisms is the project of the next chapter. 6 -95- Chapter 6: The Either-R-» Theories The desire for a syntactic basis for a language E, incorporating the EITHER mechanism informally described in Chapter 3, has led to the presentation (in Chapter 4) of the Either-R theory. It was noted that the restricted beta conversion of Either-R limits the usefulness of that theory since, for example, it prohibits the expression of recursive functions. The inadequacy of Either-R as a basis for the language E motivated the development, in the last chapter, of •-conversion. The present chapter brings these efforts to fruition in the form of the Either-R-» system, whioh consistently combines •-conversion with EITHER reduction and provides a satisfactory basis for a language E. Specifically, an Either-R-* theory shall consist of the following axioms, each of which is presented in a previous chapter: alpha. (Ch. 4) interconvertability (by renaming) of congruent expressions — e.g. (LAMBDA(X)X) • (LAMBDA(Y)Y) ; beta-R (Ch. 4) lambda conversion restricted to redexes whose arguments are in normal form — e.g. ((LAMBDA(X)X) 3)»3; various delta axioms (Ch. 4) specifying the interpretation of primitive functions and constants — e.g., (PLUS 3 5) • 8; epsj-lop (Ch. 4) contraction of E-redexes— e.g., (EITHER A B)>B (Ch. 4); lit (Ch. 4), abstraction of E-redexes — e.g. E«(EITHER E E); rho. (Ch. 4), distribution of function application over terms of an E-redex — e.g. (F (EITHER A B) )- (EITHER (F A) (F B)). fiigffla (Ch. 5) •-contraction — A>* for every expresion A. 6.1: Consistency of Either-R-» The consistency of Either-R-« may be established by techniques closely analogous to the Either-R consistency proof. Recall that the earlier proof involved the notion of enclosure, and culminated in the implication of enclosure by > —i.e., X>Y in Either-R implies X encloses Y. Extension of -96- 6.1 this technique to the present case requires that the mechanism of "-contraction be accounted for; accordingly, we extend the notion of enclosure by Defn 6.1: X " -encloses Y if, for each e-residue 1 Y' of Y, there exists an e-residue X' of X and an expression X* derived from X by •-contraction alone, such that X*=Y* in the lambda calculus. Note that we admit expressions containing the element * in the lambda calculus, treating * simply as a free variable. It is clear from the above definition that •-enclosure is transitive, and that if X encloses Y then X •-encloses Y. The following Lemma and its Corollary confirm that- •-contraction introduces no new equivalences in the conventional lambda calculus: Lemma 6.2: Let X and Y be •- and EITHER-free expressions, and let X>X« by the •-contraction of a subexpression U of X. If X # =Y in the lambda calculus, then X=Y. proof : Noting that X» contains a single • (the contractum of U), treating • as a variable in the lambda calculus gives us X=( (LAMBDA (»)X«) 0) by beta conversion. But X*=Y, hence Xr( (LAMBDA (•)Y) U) and as Y is f -free the contractum of this beta-redex is simply Y. Hence X=Y. Corollary 6.3: If X and Y are «- and EITHER-free and X»X« by a series of •-contractions, then X*=Y in the lambda calculus implies X=Y. P»"QQf is by a simple induction on the number of •-contractions in the 1 Recall Defn 4.7. 6.1 _ 9 7- reduction sequence from X to X«. The above lemma and its corollary are hardly counterintuitive in light of the developments of Chapter 5. In particular, it is clear that any occurence of « in X* must be cancelled in the derivation of Y from X, since Y is »-free. Hence we may replace such occurences by arbitrary expressions, which are still cancelled in the derivation of Y; the choice of the homologous subexpressions of X yields X=Y. The consistency proof for Either-R-« follows the format of the corresponding proof for Either-R, except that the enclosure relation in the latter proof is extended to •-enclosure in the former. The basis of this extension is given by Lemma 6.4: Let X>Y be a single reduction step in Either-R-«. Then X •-encloses Y. Proof : Lemma 4.13 establishes the lemma for the reductions allowed in Either-R; hence we need consider only the case of a •-contraction. Let U be the contracted subexpression of X. For each e-residue Y' of Y, there is a corresponding e-residue X' of X such that either X' and Y' are identical or Y' is the result of the *-contraction of an e-residue U' of U in X'. Hence X'»Y' by '-contraction, and X •-encloses Y. The following theorem is the Either-R-» analogy of Theorem 4.15: Thm 6.5: Let X and Y be expressions containing no occurrences of EITHER or «, and let X»Y in Eitlier-R-». Then X=Y in the lambda calculus. proof : By Lemma 6.4 and the transitivity of •-enclosure, X '-encloses Y. Since each of the expressions X and Y is EITHER-free, each expression is its own unique e-residue, and X»X*=Y where X>X» by •-contraction alone. By Corollary 6.3, X=Y in the lambda calculus. Thus the consistency of Either-R-* follows from the consistency of the lambda calculus. -98- 6.2 6.2: Relation of « to EITHER We have already noted that the mechanism of '-contraction leads to the interpretation of each expression A as the upper bound, in the sense of >, of a family of expressions derivable from A. To formalize the relation between such a family of expressions, we introduce the terminology of Defn 6.6: Expressions X and Y are consistent in a theory T if and only if there is an expression Z such that both Z>X and Z>Y in T. Then the R-» theories are partitioned by the consistency relation into equivalence classes, of which there are infinitely many (since there are infinitely many mutually incongruent normal forms). Then the characteristic of R-* which is established by Corollary 5.10 is that any finite set of consistent expressions in normal form has an upper bound which is also in normal form. We note that in R-» the > ordering on the set of expressions derivable from an expression A is, in general, nontrivial. Unless A is the element * the upper bound of the set, A, is distinct from the lower bound *; furthermore there may be infinitely many expressions A^A.,*... in the set such that for no j>i is A >k . This is certainly not the case in the conventional lambda calculus, in which consistency implies interconvertibility and hence equivalence. What the mechanism of '-contraction has added to the lambda calculus is a method of deriving from an expression A an approximation A» to A which is strictly weaker in the sense of >. We may. then view the * mechanism as a method of introducing new expressions which are weaker than the conventional lambda calculus expressions, as each expression in R-* is derivable from a •-free expression. In this light we must regard the EITHER construct as a mechanism for introducing stronger expressions into the lambda calculus. While R-» (and for that matter the conventional lambda calculus) contain upper bounds only for consistent sets of expressions, we can with EITHER represent the upper bounds of arbitrary (enumerable) sets of expressions. Observe further that, for 1 Or, equivalently, we may say that in the Either theories, every set of expressions is consistent. 6.2 -99- arbitrary expressions X and Y, the expression (EITHER X Y) is the least upper bound of X and Y since by Theorem 4.4, Z>X and Z>Y implies ZXEITHER X Y). This suggests that the ordering of Either-R-* expressions by > forms a complete lattice. 6.3: Evaluators for E As we have noted, interpreters for languages supporting the EITHER construct require a slightly different structure from our previous examples: the reducibility of expressions to multiple values suggests that an evaluator for E should enumerate the values of the input expression. Accordingly, we formulate the evaluator as a function E of 2 arguments, an expression X to be evaluated and a numeric index j specifying which value is to be returned. The evaluator is constructed such that, for each X and j, E[X;j] is an expression X' in normal form such that X»>X' in Either-^*. The value of E[X;j] is, in general, not defined for all values of j; it may be assumed in particular that EEX;j] is undefined for those cases of X and j not represented in the algorithm presented informally below. We again assume the existence of an invertable pairing function, and use here the notation <n;m> to denote that natural number which uniquely encodes the ordered pair of natural numbers (n,m). We make the further assumption that for no n and m is <n;m><2. E[X;j] = if j=0 then •; if X is atomic and j=1 then X? if X is of the form (LAMBDA(Y)M) then (LAMBDA(Y)E[M;n] ); if X is of the form (EITHER A B) and j=<1;n> then E[A;n]; , 2 if X is of the form (EITHER A B) and j=<2;n> then E[B;n]j if X is of the form (A B) and j =<<m;n>;p> then APPLY[E[ A;mj ;E[B;n] ;p] ; where the algorithm for APPLY is given informlly by APPLY[F;X;j] = Recall that the atomic expressions are identifiers (including primitive function symbols and variables) and numeric constants. -100- 6.3 if F is of the form (LAMBDA(Y)M) then E[S[X;Y;M] ; j] ; if (F X) is a delta-redex and j=1 then F[X]; else if j=1 then (F X); We note that E[X;j] is in normal form where it exists, and the value E[X;j] is in each case the result of an Either-R-* contraction sequence on X. Although we don't claim that the values E[X;j] of X are ordered by > for successively higher values of j, the index j specifies, roughly, which of the approximations of X is to be returned. We may envision implementations of the E interpreter which make use of massive parallelism to compute simultaneously the values of (F X) for many different approximations of X; such use of redundant computation may serve to minimize the real time required to compute an acceptable value for X. Such an implementation follows, roughly, the spirit of fast adder circuitry which computes redundantly the high order portion of a sum simultaneously with the low order portion, and then selects the correct high order- portion on the ' basis of some intermediate carry. These implementational issues are largely ignored in the present work, but present some intriguing possibilities for future research. 6.4: Summary The Either-R-* Theory may be used as the semantic basis for a language, E, which solves the specific expressibility problem demonstrated in Chapter 4. The evaluation of expressions in E lends itself naturally to the use of multiprocessing techniques which tend to minimize the total real time necessary to relize an acceptable evaluation of an expression (F X) by the simultaneous application of F to one approximation of X while computing a better approximation. While the implementation details are not pursued here, we feel that current technological developments make this area worthy of further study. 7 -101- Chapter 7: The Either-K Theories The inconsistency of EITHER distribution (Axiom rho) with the unrestricted beta conversion of the lambda calculus has motivated the restricted beta-R conversion of the systems presented thus far. This chapter explores an alternative formulation, in which EITHER distributivity is sacrificed in order to accommodate the conventional (unrestricted) beta conversion. The Either-K theories include the axioms alpha, delta, epsilon, mu, and the (unrestricted) beta axiom of the lambda calculi: Axiom beta : Let E be an expression of the form ( (LAMBPA(a_>b_)c_). Then E«E', where E' is the contractum S[cja.;.bJ . Since Either-K preserves the axioms of the lambda calculi, it is clear that the equivalence • in Either-K is a proper extension of the lambda calculus equivalence =. In this sense the Either-K calculi are closer to the conventional lambda calculi than the Either-R-* theories. There is, however, a fundamental sense in which Either-K is a more radical departure from the lambda calculi than is Either^Rr*. In the latter theories functions are ultimately applied only to normal form operands whose semantics are those of the lambda calculi. The ability, in Either-K, to apply functions to multivalued expressions (such as E-redexes) requires that we reinterpret the semantics of each function relative to these new elements of its domain. 7.1: K -abstraction By the axiom beta of the lambda calculus, the expressions M and ((LAMBDA(x) M) A) are equivalent when A is an arbitrary expression and M contains no free S is the lambda calculus substitution function given in Defn 2.6. -102- 7- 1 occurrences of the variable x. This fact is consistent with the observation that the bound variable, x, is ignored in the body of the function applied to A; hence the value of the application is independent of the value of the argument A. Despite the intuitive satisfaction with which we accept the above equivalence, the presence of functions which ignore their arguments complicates the proof of many otherwise straightforward results in the lambda calculus. Indeed, Church has argued against the inclusion of such functions in his theories, fearing at one time that they led to inconsistencies. The task of proving the consistency of the Either-K theories, to be attacked presently, is likewise complicated by the inclusion of functions which ignore their arguments. The definitions and results of this section provide the mechanism for dealing with the formation of such functions in later proofs. He begin with Defn 7.1: A K-redex is an expression of the form ((LAMBDA(x)M) A) where A is any expression and M is an expression not containing free occurrences of the variable x. Defn 7.2: A K-abstraction is a reduction step* consisting of the replacement of a subexpression M by a K-redex of the form ((LAMBDA(x)M) A) where A is any expression and x is a variable not occurring free in M. We now wish to show that the K-abs tract ions in a reduction sequence can be postponed to the end of the sequence. We introduce a term to describe reduction sequences whose K-abs tractions follow all other reductions: Defn 7.3: A reduction sequence R is K-normal if no K-abstraction in R 1 For discussion and historical insight, see Curry[12], particularly the comment at the end of Ch. 3. 2 recall Defn 4.1. 7.1 -103- precedes a reduction step which is not a K-abs tract ion. Thus a reduction sequence X (J >x 1 >...M n is K_normal if there is an i , where Q<i<n, such that the reductions X Q >...X i are not K-abs tract ions and the reductions X. >...>X^ are only K-abs tract ions. We wish to show that, for every in ' reduction sequence X_>. . .>X, there exists a K-normal reduction sequence from X to X . We begin with sequences of length 1: Thm l.k: Let X-^X^X- be a two-step reduction sequence from X Q to X-, where the reduction step X >X. is a K-abstraction and the reduction step X->Xp is not a K-abstraction. Then there is a K-normal reduction sequence from Xq to X_j containing at most one reduction step which is not a K-abstraction. proof : Let U be the subexpression of X which is replaced in the reduction step X >X.. Then U is replaced in this step by 0', an expression of the form (<LAMBDA(y)U) A) where y is a variable not occurring free in 0. We exhaustively examine classes of the reduction step X 1 >X ? : Case 1: The reduction step modifies only the subexpression A of U'; let U become A' in X ? . The K-normal sequence from X. to X, is then the single K-abstraction replacing U by < (LAMBDA (y)U) A') Case 2: The reduction step modifies only the subexpression of U'; then U becomes W in X 2 . The K-normal sequence from X Q to X~ is then: a) Replace U in X Q by W, yielding X '; b) Replace W in X Q ' by the K-redex ((LAMBDA(y)W) A) yielding J.^ Case 3: The expression U' in X 1 is replaced by U by beta reduction. Then X and X are identical expressions, and the empty reduction sequence -104- 7.1 yields X- from X Q . Case 4: The reduction step replaces some subexpression V of X 1 by the expression V', where V is not a subexpression of U' and U' is not a subexpression of V. The K-normal sequence from X to X_ is then a) The replacement of V in X by V, yielding X '; b) The replacement of U in X ' by U', yielding X_. Case 5: The expression U' is replaced by the expression (EITHER U' U'> The K-normal sequence from X to X_ is then a) The replacement of U in X Q by (EITHER U U), yielding X Q '; b) The replacement of (EITHER U U) in X Q ' by (EITHER U' U') through two consecutive K-abs tract ions. Case 6: The expression U' is replaced by the expression (EITHER ((LAMBDA(y)U) A 1 ) ULA»fflBA(y)U) A ? ) by Axiom rho. The K-normal sequence from X. to X, is then a) The replacement of U in X Q by (EITHER U), yielding X Q '; b) The replacement of (EITHER U U) in X Q ' by (EITHER ((LAMBDA(y)U) A^ ((LAIfflDA(y)U) A 2 >) through two consecutive K-abs tract ions. Case 7: The subexpression U' is replaced by an expression W of the form ((LAMBDA(z)U) A) derived from U' by alpha conversion. Then the variable z does not occur free in D, and X. may be reduoed to X_ by a single K-abs tract ion. Case 8: Some subexpression V containing U' is replaced by an expression V'. Then one of the following applies: 8a) V' is derived from V by alpha conversion.. Then we may apply that alpha-conversion to X-, yielding X ', and follow with the K-abstraction from X ' to X ? . 8b) V' contains n occurrences of 0', where n is zero or greater. Then there is a reduction of the same type from X_ to X Q ', where X ' is identical to X ? except for the n occurrences of in ■ X * corresponding to n occurrences of U' in X_. Our K-normal sequence from X Q to X_ 7.1 -105- consists of the reduction of X to X ' followed by n K-abs tract ions replacing the occurrences of U by U'. This list of cases is exhaustive, completing the proof. Theorem 7.4 shows that every two-step sequence of reductions is equivalent to some K-normal reduction sequence. The generalization of this result to sequences of n reductions is complicated by the fact that the K-normal sequence guaranteed by Theorem 7.4 may be of arbitrary length, thus ruling out a simple induction on the length n of the reduction sequence. Lemma 7.5: Let R be a reduction sequence f ran X. to X containing exactly 1 reduction step which is not a K-abs tract ion. Then there is a K-normal reduction sequence from L to X , v n proof : by induction on the length n of tile reduction sequence R. £Mis_: Trivially true for n<2} for n=2, guaranteed by Theorem 7.4. induction : Let X Q >X >.. ,>X be the reduction sequence R. If the step X Q >X 1 is not a K-abs tract ion, then R is K-normal; hence we may assume that X >Xv is a K-abs tract ion. Then a single step of the subsequence X >...>X is not a K-abs tract ion; by the inductive hypothesis, there is a K-normal reduction sequence X,>Y >Y >...« of which only the reduction step X,>Y Q may be other than a K-abs traction. But by Theorem 7.4, there is a K-normal sequence X «0>.,.>Y equivalent to the sequence X >X 1 >Y Q ; thus the reduction sequence X n «0>. ..>Y_>. ..« is K-normal fromX. to X . <* v n On t)efn 7.6: The K- index of a reduction sequence R is the number of non-K-abs tract ion steps in R which follow the first K-abstraction in R. If R contains no K-abs tractions, then the K-index of R is zero. Note that the K-index of a reduction sequence R is zero if and only if R is K-normal, We shall base the induction in the proof of the next theorem on the K-index of the reduction sequence to which it is applied. -106- 7.1 Thm 7.7: Let R be a reduction sequence from X to X . Then there is a K-normal reduction sequence from X to X . proof is by induction on the K-index of R. basis ; If the K-index of R is zero, then R is K-normal. induction : The K-index n of R is greater than zero. Let X_>. . .>X denote u ft R, and let Xj^X^ be the first K-abstraetion in R. Let X,»X. j be the first reduction step following X^X^ in R which is not a K-abs tract ion; the existence of such a j is assured by the K-index of R. Then the subsequence X »X .j>. . ,>X « of R contains a single step which is not a K-abs tract ion; by Lemma 7.5 there is a K-normal sequence X >Y-». ..*X. - from X. to X. .. Then the sequence R" given by X Q >. . .>X.>Y_>. ..>X, ^2,. ..X has a K-index of n-t. By the induction hypothesis, there is a K-normal sequence from X. to X . ID It follows from Theorem 7.7 that every reduction sequence may be reordered in such a way that every K-abs tract ion follows every reduction step which is not a K-abs tract ion. Curry[12] refers to expressions as fictitious if they appear as the arguments of K-redexes; hence A is a fictitious subexpression of B if A is cancelled in the evaluation of B. Theorem 7.7 asserts that the introduction of fictitious subexpressions can be postponed to the end of a reduction sequence. Consider the following expressions: Z =. (LAhffiBA(X)3> A =. ((LAMBDA(H)(H H))(LAJffl»A(H){H H)) I =. (LAMBDA(X)X) Then the reduction sequence 3 > (Z A) MI (Z A)) is not K-normal, since the K-abstraction 3>(Z A) precedes the beta abstraction (Z A»(I (Z A)). We may, however, reorder the sequence so that the fictitious subexpression A is introduced in the last reduction step; the resulting reduction sequence 3 > (I 3) MI (Z A)) is K-normal. 7.2 -107- 7.2: Consistency of Either-K Theories It was noted, following the proof of the consistency of the Either-R theories, that the technique used there was inapplicable to the Either-K axioms since unrestricted beta conversion does not preserve the enclosure relation. We avoid this difficulty in the corresponding proof for the Either-K theories by arranging the reduction sequence of an EITHER-free expression so as to ensure that arguments in beta contractions are unitary. Since the Either-K reduction sequence of an EITHER-free expression can introduce non-unitary subexpressions only through K-abs tract ion, the result of the preceding section provides a critical step in the present proof. We begin by distinguishing expressions containing only unitary subexpressions: Defn 7.8: An expression X is pure if every subexpression of X, includitig X itself, is unitary. Note in. particular that every EITHER-free expression Is pure. We now precede to the major task of this section, which is the proof that the reductions permitted by our axioms preserve purity of expressions. We begin with the case of beta-contractions: Lemma 7.9: Let Y be EITHER-free and let X be a pure beta-redex of the form <(LAtfflDA(y)B) A) such that for each e-residue X' of X, X'=Y. If Z is the result of lambda conversion on X {ie, Z is the result of substituting A for each free y in B), then for every e-residue Z' of Z, Z'~Y. proof : Let Z' be an e-residue of Z. Then Z' contains zero or more occurrences of A p a 2 , ..., A n where each ^ is an e-residue of A. By the purity of X, A is unitary, hence each A. is convertible to Aj Z'=Z" where Z" is the result of lambda conversion on <(LA»fflDA(y)B') A^ where B' is some e-residue of B. Hence Z"=Y, and Z'=Y. Thus -108- 7.2 Lemma 7.10: Let X, Y, Z, and Z' be as in Lemma 7.9, above. Then Z is pure. proof : Let U be an arbitrary subexpression of Z, and let W be the corresponding subexpression of B. If W contains no occurrences of y which are free with respect to X, then W and U are identical, hence U is unitary by the purity of X. If H contains such occurrences of y, then U is the result of lambda conversion on ((LAMBDA(y)H) A) and, by Lemma 7.9, U is unitary. We next show that beta abstractions preserve purity, so long as they are not K-a bs tract ions : Lemma 7.11: Let Z be a pure expression containing 1 or more occurrences of the subexpression A. Let W be a beta -red ex of the form ( (LAMBDA (I )B) A) such that the contractum of W is Z. Then W is pure and, for every e-residue W' of W there exists an e-residue Z' of Z such that W'=Z'. proof : Since A is a subexpression of the pure expression Z, A is unitary; let the e-residues A ' A 2 ',...A. ' of A each be convertible to A' in the lambda calculus. For each e-residue B' of B there is a corresponding e-residue Z' of Z, such that Z' contains some A ' in place of each free occurrence of Y in B; hence Z'=S[A';y;B']. Each e-residue W is of the form ((LA i 'MBDA i '(Y)B')A i ') where B' is an e-residue of B; but then W is convertible to S[A';y;B']=Z'. Thus each e-residue W' of W is convertible to an e-residue Z' of Z. Noting that homologous subexpressions B1 and Z1 of B and Z, respectively, are either identical or related by Z1=S[A';Y;B1], we deduce by the above argument and the purity of Z that B is pure. Hence W is pure. Note that Lemma 7.11 fails to hold for K-a bs tractions; consider, for example, the K-abs traction 7.2 -109- M>( (LAMBDA (X)M) (EITHER 2 3)) where M contains no free occurrences of the variable X. Clearly the abstraction of M is impure regardless of the purity of M. We now present the principal result of this section, from which the consistency of the Either-R axioms follows directly: Lemma 7.12: Let X»Y be a single reduction step other than a K-abstraction in Either-K, and let X be pure. Then Y is pure and X encloses Y. proof: The cases where X»Y is a beta conversion follow directly from Lemmas 7.9, 7.10, and 7.11; and if the step is an alpha conversion, the e-residues of Y are clearly congruent to the e-residues of X, and Y is pure. If X»Y is a delta conversion then both X and Y are EITHER-free and the lemma is trivially true. If X>Y is an EITHER-conversion in either direction, the purity of Y follows fr'm the purity of X and the e-residues of X and Y are identical. The consistency of the Either-K theories is presented as Thm 7.13: Let X and Y be EITHER-free expressions, and let X»Y in Either-K. Then X=Y in the lambda calculus. proof: From Theorem 7.7, we may assume that there is a K-normal reduction sequence from X to Y; let X>. ..M^T^. . .>Y be such a sequence, where the subsequence X»...>Y Q contains no K-abs tract ions and Y >...>Y contains only K-abstractions. Then Y Q must be EITHEB-free, since each of the K-abs tractions Y^Y^ can only increase the number of EITHER redexes, and Y is EITHER-free. Y q= y in the lambda calculus since each of the conversions Y Q >...>Y is a valid beta conversion. By Lemma 7.12, X must enclose Y Q since X is pure; but each of these expressions is EITHER-free and hence is its own e-residue. Thus X=Y.=Y. Corollary 7.14: Let X and Y be EITHER-free expressions, and let X-Y in Either-K. Then X=Y in the lambda calculus. -110- 7.2 Proof : Directly from Corollary 7.13. 7.3: Functional Domains of Either-K The semantics of the Either-K Theories bear a superficial similarity to those of the corresponding Either-R-« Theories: in each case a functional domain F of the lambda calculus is extended to a domain F* whose elements are enumerable subsets of F. The question of restrictions on beta conversion seems, at first glance, to be an issue of evaluation order whose semantic ramifications parallel, say, those of the applicative /normal order distinction. While this analogy can be defended, as it has been in earlier sections of this thesis, there is evidence suggesting that the distinction between the Either-R and Either-K semantics is of a rather more fundamental nature. The distributivity of function application over EITHER terms, sanctioned in the Either-R Theories by Axiom rho, constitutes a limitation on the expressive power of languages built on these theories. Consider, for example, the function f whose informal definition is f[x] = x+x; which computes, in the lambda calculus, a numeric value which is twice the value of its argument x. Our experience with conventional applicative languages reinforces an intuitive expectation that f will have only even numbers in its range (assuming that the domain of f is the set of natural numbers). The natural extension of our intuition to the Either-R Theories is consistent with the range of f there,, containing enumerable sets of even numbers. In the Either-K Theories, however, we must realign our intuition. The application of f to the argument eitherE2;3l, for example, is reducible in Either-K to any of the numbers in {4,5,6} rather than the {4,6} result of Either-R. Thus although the semantics of the application of functions to single-valued arguments remains consistent with the lambda calculus, the behavior of functions with multivalued arguments differs between the Either-R and Either-K systems. 7.3 -111- A more bizarre demonstration of this difference is the function g. defined informally by g[x] = if x >x then 1; else 0; which, in the lambda and Either-R calculi is equivalent to the single argument constant function which always returns zero. Yet the Either-K reduction of g[either[1;2]] yields the values {0,1}, even though g[1] and g[2] each evaluate to {0}. Since the behavior of g in Either-K violates the distributivity axiom of the Either-R Theories, we clearly cannot express in these theories a function with the properties of g; yet g appears to be a computable function definable on the domain F*. 7.4: Summary This chapter presents a consistent theory which combines EITHER conversion with unrestricted beta conversion. This combination requires 1) that we abandon the distributivity of functions over EITHER terms, and 2) that we reinterpret the semantics of EITHER. The latter reinterpretation is only hinted at in this chapter, and we confess that the semantics of the Either-K theories require further study. This empty page was substituted for a blank page in the original document. 8 -113- Chapter 8: Summary and Conclusions There has been a definite tendency, in the course of the work reported here, to provide questions much more frequently than answers. We regard this situation, perhaps 'defensively, as a healthy attribute of research in a field as theoretically immature as the science of programming languages. 8.1: Summary The general topic of this thesis is the correspondence between the syntactic mechanism of an interpreter and the semantic structure of the language it interprets. The restriction of this study to the class of applicative languages is defended, in Chapter 1, on the grounds that i) Interpretive mechanism for applicative languages is simple, since such complications as assignment, side effects, and transfers of eontrol are avoided; ii) The semantics of applicative languages are independent of the notion of time; iii) The theories of mathematical functions may serve as a semantic basis for applicative languages. Expressions of an applicative language are viewed as representations of objects in an abstract semantid functional domain containing functions and constants, and expressions are semantically equivalent if they represent the same abstract element. The stack- and tree-environment interpreters presented in Chapter 2 illustrate semantic limitations imposed by typical compromises between efficiency and expressive power. The defect of S must be viewed as an interpreter "bug" if we take mathematical functions as a semantic basis, since certain expressions are interpreted by S in a manner inconsistent with the behavior of functions. The T interpreter of Chapter 2 relates the issue of evaluation order to the expressibility of certain functions. The applicative order evaluation of T, i.e., the FUNARG problem. -114- 8 - 1 in which arguments to a function are evaluated before the application of the function, is seen to lead to the inexpressibility of functions which ignore the value of their arguments. This motivates a preference for the normal order evaluation of the N model, in which such functions are expressible. The demonstration in chapter 2 of a functional domain F of N assures us that every expression is interpreted by N in a way that is consistent with our functional semantics; it does not, however, establish that every valid semantic element (e.g. , every computable function defined on the semantic domain of N) is expressible in N, Chapter 3 demonstrates a function, WHICHFF, which despite its computability is expressible neither in N nor in the lambda calculus. The expressibllity of WHICHFF seems to require a mechanism analogous to multiprocessing, and two therapeutic language extensions are considered: i) A "coding" primitive which allows a program access to the representation of a function supplied as its argument; and ii) A primitive EITHER whose interpretation involves the dovetailed evaluation of its arguments. The admission of coding essentially abandons all semantic constraints and allows the programmer to reinterpret expressions as he wishes; we thus discard this alternative as semantic anarchy. The EITHER primitive may be justified in terms of applicative semantics, however, by the expansion of the semantic domain F into the power set F* , each of whose elements is a subset of F. Thus once EITHER is introduced we must semantical ly associate each expression X with an enumerable set of abstract values or "meanings* of X. Such a multivalued semantic domain is necessary to reconcile the function WHICHFF with applicative language semantics. The semantic domain F* motivated in Chapter 3 is suggestive of a complete lattice ordered by set theoretic inclusion. The undefined (or nonterminating) computation is naturally associated with the empty set in F*, and that expression TOP whose values include the entire domain of the lambda calculus corresponds to the maximal element of F». The semantic element associated with the expression either[a;b] becomes the union of the respective F* elements corresponding to the expressions a and b. 8.1 -1 15- In Chapter 4 our attention returns to the subject of interpretive mechanisms. In particular we desire a formalism for syntactic manipulation of expressions in a language including EITHER, reflecting the insight gained through informal scrutiny of the structure of F« in Chapter 3. The formalisms introduced in Chapters 4-7 are systems of conversion axioms, similar to (and based on) the lambda calculus; each system (or theory) defines an ordering, >, corresponding to inclusion in F» — thus, for example, either[a;b]>a and either [a ;b]»b in each system. A complication arising in Chapter 4 involves the reconciliation of the beta reduction of the lambda calculus with the intuitively motivated requirement that functions be distributive over EITHER terms — i.e., that f [either[a;b] ] be equivalent to either[f[a] ;f[b]]. The EITHER-R system presented in Chapter 4 resolves this difficulty by restricting beta conversion to arguments which are reduced to normal form; while consistent, the resulting theory is too weak to be useful. The syntactic mechanism of *-conversion, presented in Chapter 5, solves this problem of Either-R. Chapter 5 introduces the expression * as a canonical (normal form) representation of the undefined computation, and extends the ordering > so that the syntactic significance of * (k>* for every expression A) reflects the semantic significance of the undefined computation (the empty set is a subset of every element of F»). The use of '-reduction allows every expression, including the single-valued expressions of the conventional lambda calculus, to be reduced to multiple normal forms. The R-* theory developed in Chapter 5 reinforces an interpretation of the normal forms derivable from an expression X as approximations to X, and shows that for any context A{X} having normal form value A' there exists a sufficiently good (normal form) approximation X* of X such that A{X»} also has the value A'. This result has major semantic consequences; in particular, it implies that meaning of an expression X is completely characterized by the set of normal forms derivable (in. R-») from X. Moreover the result is shown to carry over to the conventional lambda calculus, since every normal form derivable in the lambda calculus is derivable in R-*. The extensional semantic equivalence relation Informally, beta reduction is the application of a lambda expression thrh«1nS ^ir^?2 t fn n J^ y K^ bst ^ t ^ i0 ? °L its arguo?nt for free occurences of tne bound variable in the body of the lambda expression. -116- 8.1 suggested by these findings, namely the interconvertability of normal forms derivable in R-*, is demonstrated by showing the equivalence of non-interconvertable expressions for the fixed point operator Y. The mechanisms of "-conversion and EITHER-reduction are combined, in Chapter 6, to yield the Either-R-* system. The respective functions of the two mechanisms are, in a sense, complementary; roughly speaking EITHER allows expressions to be combined to make "stronger" expressions while "-conversion allows expressions to be resolved into weaker component expressions. The Either-R-* system is consistent, retains the power of the lambda calculus, and interprets EITHER according to the semantic notions of Chapter 3. We thus view Either-R-» as a practical syntactic basis for the construction of for interpreters of languages based on multivalued semantic domains; such an interpreter, E, is presented at the end of Chapter 6. Chapter 7 explores an alternative resolution of the conflict between unrestricted beta conversion and the distributivity of functions over EITHER terms. The Either-K system presented in that chapter sacrifices such distributivity in order to allow the unrestricted beta conversion of the lambda calculus. While this combination results in a consistent theory (as demonstrated in Chapter 7) it leads to a semantic structure which is fundamentally different from that of the Either-R theories, in particular regarding the application of functions to multivalued arguments. 8.2: Conclusions The study of applicative languages from the complementary viewpoints of interpretive and semantic structure leads synergistically , we feel, to a new insight in each area. We have repeatedly found the syntactic mechanisms and semantic structures to be mutually illuminating, and view this dual perspective as a principal influence on the direction and motivation of this thesis. The following are viewed as the principal results of this thesis: 1) The motivation and presentation of an applicative model of multiprocessing. The applicative approach to this mechanism has certain 8.2 -117- technical advantages over conventional formulations; notable among these is the complete irrelevance of time as a parameter of language semantics. The corollary disadvantage of the applicative model is its uselessness in the study of time dependent implementation considerations — such as scheduling, deadlocks, and synchrony of processes. 2) The formulation of the semantic domain F* for multivalued applicative languages. We find particularly interesting the potential extension of the Scott formalism which F* suggests: we have added, to the Scott domain, unique upper bounds of arbitrary sets of semantically distinct elements. The lack of such upper bounds in the Scott model has been conspicuous, and the EITHER construct presented here seems to provide a natural interpretation for them. 3) The mechanism of *-conversion and the results relating it to the conventional lambda calculus. These results augment the lambda calculus with a syntactic substructure (i.e., the ordering under >) which bears close analogy to the semantic structure developed by Scott. In addition, •-conversion provides a concrete (syntactic) relation of semantic equivalence which may illuminate the relationship between lambda calculus expressions having no normal forms. 4) The presentation of consistent theories of EITHER conversion. The analyses of these systems is by no means exhaustive; we have not shown, for example, that no axiom is derivable from the remaining axioms. The theories do, however, provide sufficiently powerful syntactic mechanism that interpreters may realistically be based upon them. 8.3: Directions of Future Research We recognize that this section constitutes fertile grounds for an essay strewn with universal quantifiers. Restricting our attention to specific questions left unanswered by this work, we find most demanding of further attention: 1) The relative expressive power of EITHER-augmented versus CODE-augmented ( languages. We conjecture that every computable function defined on the single-valued domain of the lambda calculus is expressible in the language E, and have in fact spent considerable effort in trying -118- 8.3 (unsuccessfully) to prove this conjecture. The discovery of computable functions expressible (with coding) in C but inexpressible (with EITHER) in E would be counterintuitive and somewhat depressing. 2) The semantics and expressive power of languages based on the Either-K Theories. The presence of functions which compute different results for a multivalued argument X than for singlevalued components of X raises new fundamental questions: what is a computable function on F*? Are the Either-K Theories functionally complete? If not (and we are pessimistic on that issue) which functions are not expressible in Either-K?- 3) There appears to be a great deal of room for further development of the theories of EITHER conversion. The extension of these theories to allow eta reduction seems feasible. Further extensions may make the extensional relation of semantic equivalence tractable by syntactic means alone, e.g. by axiomatically asserting in Either-R-* the equivalence of expressions whose normal forms are interconvertable. 4) The area of interpretive mechanisms for EITHER-based languages has some interesting possibilities. The techniques of computational complexity studies, for example, might yield some quantitative bounds on the computation time necessary for the evaluation of classes of applicative expressions. As the cost of computation power continues to plummet, methods for making use of massive parallelism becomes a practical as well as academic interest. 5) The relationship between the mechanisms of EITHER- and *-conversion and the semantic constructions of Scott demand more serious attention than the informal parallels drawn here. Much of Scott's important work seems to bear rather directly on the systems presented here, and we recognize that too little advantage has been taken of this resource. It must finally be acknowledged that our quest for a functionally complete language — one whose domain D contains every computable function defined on D — has not been an unqualified success. The lambda calculus, whose functional completeness was suspect, was scrutinized and found to be incapable of expressing certain functions (e.g. WHICHFF). To remedy this inadequacy, the lambda calculus was extended via the EITHER construct; the result (the Either 8.3 -119- theories) is, indeed, capable of expressing WHICHFF. However, the new systems have additional elements in their domain, so that the functional completeness of the Either theories is again suspect. The results of this thesis, then, suggest a similar program of scrutiny and extension to repair their inadequacies. There is an inevitable circularity in this course of research, mitigated by the fact that each cycle allows us to see previous cycles more clearly. A way a lone a last a loved along the/ riverrun, past Eves and Adam s, from swerve of shore to bend of bay, brings us by a commodius vicus of recirculation back to Howthe Castle and Environs. -Finnegan's Hake, last/first lines -120- 9 References [I] Church, A.. The Calculi of Lambda Conversi o n . Annals of Mathematics St udi es, Princeton university Press 19 1 *! . [2] Landin, P, "A lambda -cal cuius Approach" In Advances in Programming and Non-numerical Computation. Peraagon Press, NewTork 19ob. [3] Dertouzos, M.. Structure and Interpretation of Computer Languages (class [4] Perils, A. J., "The Synthesis of Algorithmic Systems", JACM, January 1967. [5] ^.^ftgHl^flllJli^ Technical [6] Scott, D. , The La ttice of Floy Diagrams. Technical monograph PRG-3, Oxford University November 1970. [7] Hoare, C. A. R. , "Procedures and Parameters: An Axiomatic Approach". Lecture Rotes in Mathematics 188, Springer-Verlag, Berlin 1971. t8] ^"^t^C^^^HM^^W^f- [9] Cooper, D. C. , "Program Schemes, Programs and Logic". Lecture Notes in Mathematics 188. Springer-Verlag, Berlin, 1971. [10] Moses. J., "The Function of FUNCTION in LISP (or, Mhy the FUNARG Problem Should Be Called the Environment Problem)", SIGSAM Bulletin 15, July 1970. [II] Rosenblocn, P. C. , The |lementsof Mathematical Logic. Dover [12] Curry, H. B., and Feys, R. , Combinatory Logic. Amsterdam, 1958. [13] Paterson, M.S., "Program Schemata", Machine Intelligence III. Edinburgh University Press 1968. [14] Strachey. C. , "Fundamental Concepts in Programming Languages", NATO Conference, Copenhagen, 1967. [15] Morris, J., j^«hd«-nainul»s Mr^elg flf PrffffTgWlnff Languages. PhD Thesis, [16] Schwartz, J.T. , "Semantic Definition Methods and the Evolution of Programming Languages" in ESEMl Semantics St Pr»ff' , flTlBl I, P Languages, Prentice-Hall 1972. [17] Ershov, A.P. , "Theory of Program Schemata", IFIP Congress 71, August [18] Landin, P.J. , "The Next 700 Programming Languages", C ACM March 1966. [19] Wegner, P., "Programming Language Semantics", in Formal Semantics pf Prv T n ftffiff1nfr Languages. Prentice-Hall 1972. [20] Boehm, C. "Alcune Proprieta Delle Forme beta-eta -norma li nel lambda -K-calculo," Consiglio nazionale deile ricera Roma 696, 1968. [21] Hindley. J.R. et al, Introduction to Combinatory Logic. Cambridge UnlversityPress 1972. [22] Scott, D. "Lattice Theory, Data Types and Semantics" in Formal Semantics of Programming Languages. Prentice-Hall 1972. ■121- [23] Weizenbaum. J. "The FUNARG Problem Explained", unpublished memorandum, MIT 1968. [24] Walk, K. et al , "Abstract Syntax and Interpretation of PL/1, Version III," IBM Laboratory, Vienna TR25.098, 1969. [25] Floyd, R W. "Assigning Meanings to Programs," Proc. Symposium on Appl. Math, volume 19, 1967. [26] McCarthy, J. et al , The LISP 1.5 Programming Manual MIT Press 1965. [27] Curry, H. B. et al , Combinatory Logic vol. II, Amsterdam, 1972. This empty page was substituted for a blank page in the original document.